proposition: Lemma noduplicates_app_inv : forall l1 l2, noduplicates (l1 ++ l2) -> noduplicates l1 /\ noduplicates l2 /\ ~ (exists x, mem x l1 /\ mem x l2).
proof: Proof. Proof using. introv ND. splits. { induction l1. { constructors. } { rew_list in ND. inverts ND as ND1 ND2. rewrite mem_app_eq in ND1. rew_logic* in ND1. } } { induction l1; rew_list in ND. { auto. } { inverts~ ND. } } { introv (x&I1&I2). induction I1; rew_list in ND. { inverts ND as ND1 ND2. false ND1. apply* mem_app. } { apply IHI1. inverts~ ND. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)