Expand test coverage of proofmode
The proof mode tests don't cover the following:
-
iRename
-
iTypeOf
-
iInduction
's ability to freshen the inductive hypothesis
I have tests for the first two on my bytes-ident branch.
The proof mode tests don't cover the following:
iRename
iTypeOf
iInduction
's ability to freshen the inductive hypothesisI have tests for the first two on my bytes-ident branch.