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