fact: Fixpoint removeElem (el: A) (l: list A) : list A := match l with | nil => nil | hd::tl => match eqA_dec el hd with | left _ => tl | right _ => hd::removeElem el tl end end.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)