fact: Fixpoint removes (l m : list A) : list A := match m with | nil => nil | x :: m' => match In_dec x l with | left _ => removes l m' | right _ => x :: removes l m' end end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)