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