proposition: Fact Forall2_app_inv_l X Y R l1 l2 m : @Forall2 X Y R (l1++l2) m -> { m1 : _ & { m2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ m = m1++m2 } }.
proof: Proof. revert l2 m; induction l1 as [ | x l1 IH ]; simpl; intros l2 m H. exists nil, m; repeat split; auto. destruct m as [ | y m ]. apply Forall2_nil_inv_r in H; discriminate H. apply Forall2_cons_inv in H; destruct H as [ H1 H2 ]. apply IH in H2. destruct H2 as (m1 & m2 & H2 & H3 & H4); subst m. exists (y::m1), m2; repeat split; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)