proposition: Fact list_app_eq_inv X (l1 l2 r1 r2 : list X) : l1++r1 = l2++r2 -> { m | l1++m = l2 /\ r1 = m++r2 } + { m | l2++m = l1 /\ r2 = m++r1 }.
proof: Proof. revert l2 r1 r2; induction l1 as [ | x l1 IH ]. intros; left; exists l2; auto. intros [ | y l2 ] r1 r2; simpl; intros H. right; exists (x::l1); auto. inversion H. destruct (IH l2 r1 r2) as [ (m & Hm) | (m & Hm) ]; auto; [ left | right ]; exists m; split; f_equal; tauto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)