Skip to content

treat Forall2 constructors like we treat Forall constructors

Ralf Jung requested to merge ralf/Forall2 into master

In particular, have a lemma Forall2_cons that is an .

For consistency, rename Forall2_cons_inv to Forall2_cons_1 (matching Forall_cons_1).

Someone should probably do the same for Forall3...

Edited by Ralf Jung

Merge request reports