proposition: Lemma one_eq_app : [ x ] ++ l1 = l2 ++ l3 -> (exists qs, l2 = x :: qs /\ l1 = qs ++ l3) \/ (l2 = nil /\ l3 = x :: l1).
proof: Proof. simpl. auto using CoqListFacts.cons_eq_app. Qed.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.MetatheoryAtom Metalib.LibTactics