-
Robbert Krebbers authored
Also, rewrite `iIntoEmpValid`. Now, instead of using Ltac to traverse the type of the term and generate goals for the premises, we repeatedly apply a series of lemmas. This has the advantage that it works up to convertability, and we no longer need the `eval ...` hacks.
97deecba