proposition: Theorem Forall2_cons_iff : forall x y l l', Forall2 (x :: l) (y :: l') <-> R x y /\ Forall2 l l'.
proof: Proof. intros x y l l'. split. - intros H. now inversion H. - intros [? ?]. now constructor. Qed.
imports: PeanoNat