]> matita.cs.unibo.it Git - helm.git/search
- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal...