proposition: Lemma In_nodup_elim (x : A) : forall l, In x l -> nodup l -> exists l1 l2, l = l1 ++ x :: l2 /\ ~In x l1 /\ ~In x l2.
proof: Proof. induction l; simpl. tauto. intros [h|h] [h1 h2]. subst. exists nil. ex l. auto. destruct (IHl h h2) as [l1 [l2 [i1 [i2 i3]]]]. assert (i : x<>a). intro; subst. tauto. ex (a::l1) l2. subst. fo. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)