proposition: Fact list_cons_app_cons_eq_inv X (l2 r1 r2 : list X) x y : x::r1 = l2++y::r2 -> (l2 = nil /\ x = y /\ r1 = r2) + { m | l2 = x::m /\ r1 = m++y::r2 }.
proof: Proof. intros H. destruct l2 as [ | z m ]; simpl in H. + left; inversion H; auto. + right; exists m; inversion H; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)