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