proposition: Lemma notin_remove : forall x l, In x (remove x l) -> False.
proof: Proof. induction l; simpl. auto. destruct (eq_dec a x). auto. simpl. tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)