proposition: Lemma cut_head : forall (x : A) l, In x l -> cut x l = x::(tail (cut x l)).
proof: Proof. induction l; simpl; intros. contr. destruct (eq_dec x a). simpl. rewrite e. trivial. destruct H. rewrite H in n. tauto. tauto. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)