proposition: Lemma Forall2_last_eq : forall P r s x y, Forall2 P (r & x) (s & y) = (Forall2 P r s /\ P x y).
proof: Proof. Proof using. intros. extens. iff M (M1&M2). { lets E: Forall2_inv_length M. rew_list in E. rewrite~ Forall2_app_eq in M. destruct M as (M1&M2). inverts* M2. } { applys~ Forall2_last. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)