proposition: Fact list_app_cons_eq_inv X (l1 l2 r1 r2 : list X) x : l1++r1 = l2++x::r2 -> { m | l1++m = l2 /\ r1 = m++x::r2 } + { m | l2++x::m = l1 /\ r2 = m++r1 }.
proof: Proof. intros H. apply list_app_eq_inv in H. destruct H as [ H | (m & H1 & H2) ]; auto. destruct m as [ | y m ]. left; exists nil; simpl in *; split; auto. revert H1; do 2 rewrite app_nil_r; auto. inversion H2; subst. right; exists m; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)