proposition: Lemma incl_removes : forall l m, removes l m [= m.
proof: Proof. unfold incl. induction m; simpl. contr. case (In_dec a l). intros. right. apply IHm. hyp. simpl. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)