proposition: Lemma Forall2_last_l_inv : forall P r1 s x, Forall2 P (r1 & x) s -> exists s1 y, s = s1 & y /\ P x y /\ Forall2 P r1 s1.
proof: Proof. Proof using. introv M. forwards (y&s1&E): list_neq_nil_inv_last s. { intro_subst. inverts M. applys* nil_eq_last_inv. } subst s. rewrite* Forall2_last_eq in M. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)