treat Forall2 constructors like we treat Forall constructors

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...