fact: Fixpoint remove1 {A} (eq_dec : forall x y, {x = y} + {x <> y}) (x : A) l : list A := match l with | [] => [] | y :: tl => if eq_dec x y then tl else y :: remove1 eq_dec x tl end.
imports: Arith List Permutation