Better handling of `let` bindings in proof mode
- Make sure that
iStartProof
fails with a proper error message on goals withlet
. Theselet
s should either besimpl
ed or introduced into the Coq context. - Normalize statements before
iIntoValid
. This makes sure thatiApply
works reliable when the lemma statement involves alet
.
This fixes #520 (closed).
The MR includes some test cases.
Edited by Ralf Jung