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