fact: Fixpoint removePresent (A : Set)(eqd : eq_dec A)(u ls : list A) := match ls with | nil => nil | a' :: ls' => ls'' <- removePresent eqd u ls'; if (in_dec eqd a' u) then ls'' else (a' :: ls'') end.
imports: FCF.FCF Permutation