proposition: Lemma nodup_app_elim : forall l m : list A, nodup (l ++ m) -> nodup l /\ nodup m /\ forall x, In x l -> ~In x m.
proof: Proof. induction l; simpl; intros. intuition. destruct H. ded (IHl m H0). decomp H1. intuition. subst a. apply H. apply in_appr. exact H3. apply (H5 x); hyp. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)