fact: Fixpoint removeFirst(A : Set)(eqd : eq_dec A)(ls : list A) a := match ls with | nil => nil | a' :: ls' => if (eqd a a') then ls' else a' :: (removeFirst eqd ls' a) end.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool