Statement used to prove itself

[joneugster]

There are at least two issues concerning structural recursion of exercises:

1. Once a statement is proven, it can be used in previous levels. E.g. proof add_comm then go back two levels and now you can use add_comm to proof e.g. zero_mul. Is the (only?) solution to disable the storage of "known theorems" in local storage?
2. One should never be able to do any such structural recursive proofs. Usually, Lean would catch this, but the way we proof a new statement with everything imported makes this very hard to check, I believe.

[joneugster]

Partially fixed: we check now that a theorem cannot be used to prove itself.

You can still do trickery like proving add_comm using zero_add and then reproving zero_add using add_comm. Closing this latter issue as "wont fix"