proposition: Lemma noduplicates_app : forall l1 l2, noduplicates l1 -> noduplicates l2 -> (forall x, mem x l1 -> mem x l2 -> False) -> noduplicates (l1 ++ l2).
proof: Proof. Proof using. Hint Constructors mem. intros l1. induction l1; introv N1 N2 EQ; rew_list. { auto. } { inverts N1 as N N1'. constructors. { rewrite mem_app_eq. rew_logic*. } { applys~ IHl1. introv Mx1 Mx2. applys* EQ x. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)