proposition: Lemma remove_In : forall a x l, In a (remove x l) -> In a l.
proof: Proof. induction l;intros. simpl in *. auto. simpl in H. destruct (eq_dec a0 x). subst; simpl; right; auto. simpl in *; tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)