proposition: Lemma Forall2_cons_eq : forall P x y r s, Forall2 P (x::r) (y::s) = (P x y /\ Forall2 P r s).
proof: Proof. Proof using. intros. extens. iff M (M1&M2). { inverts* M. } { auto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)