proposition: Lemma incl_remove2 (x : A) : forall l, remove x l [= l.
proof: Proof. induction l; simpl. refl. destruct (eq_dec a x). apply incl_tl. hyp. apply cons_incl. refl. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)