>you don't need to anything more than this

You also have to check for things like sorry or defining axioms.