proposition: Lemma incl_removes_app : forall l m, m [= removes l m ++ l.
proof: Proof. unfold incl. induction m; simpl. contr. intros. destruct H. subst a0. case (In_dec a l); intro. apply in_appr. hyp. simpl. auto. case (In_dec a l); intro. apply IHm. hyp. simpl. case (eqdec a a0); intro. subst a0. auto. right. apply IHm. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)