proposition: Lemma In_remove : forall (x y : A) l, x <> y -> In y l -> In y (remove x l).
proof: Proof. induction l; simpl; intros. hyp. destruct (eq_dec a x); destruct H0. rewrite e in H0. tauto. tauto. rewrite H0. simpl. tauto. simpl. tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)