proposition: Fact app_eq_single_inv X (l m : list X) x : l++m = x::nil -> l = nil /\ m = x::nil \/ l = x::nil /\ m = nil.
proof: Proof. intros H. destruct l as [ | y l ]; auto. right. inversion H. destruct l; destruct m; auto; discriminate. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL ill_cll)