proposition: Lemma remove_notin (x : A) : forall l, ~In x l -> remove x l = l.
proof: Proof. induction l; intro nxl; simpl. refl. destruct (eq_dec a x). subst. fo. f_equal. fo. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)