proposition: Lemma Forall2_app_eq : forall r1 r2 s1 s2 P, length r1 = length s1 -> Forall2 P (r1 ++ r2) (s1 ++ s2) = (Forall2 P r1 s1 /\ Forall2 P r2 s2).
proof: Proof. Proof using. intros r1. induction r1; introv E; destruct s1; tryfalse; rew_list in *; extens. { autos*. } { iff M (M1&M2). { inverts M as N1 N2. rewrite* IHr1 in N2. } { inverts M1. constructors~. rewrite* IHr1. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)