proposition: Fact Forall2_cons_inv_l X Y R a ll mm : @Forall2 X Y R (a::ll) mm -> { b : _ & { mm' | R a b /\ mm = b::mm' /\ Forall2 R ll mm' } }.
proof: Proof. intros H. apply Forall2_app_inv_l with (l1 := a::nil) (l2 := ll) in H. destruct H as (l & mm' & H1 & H2 & H3). destruct l as [ | y l ]. exfalso; inversion H1. apply Forall2_cons_inv in H1. destruct H1 as [ H1 H4 ]. apply Forall2_nil_inv_l in H4; subst l. exists y, mm'; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)