proposition: Lemma permutation_remove1 {A} eq_dec (a : A) l l' : Permutation l l' -> Permutation (remove1 eq_dec a l) (remove1 eq_dec a l').
proof: Proof. intros HP. induction HP as [| x p IHp | x y | l'' p1 p2 IHp1 IHp2]. - constructor. - simpl. destruct (eq_dec _ _). auto. constructor. auto. - simpl. destruct (eq_dec _ x), (eq_dec _ y); subst; constructor. all: apply Permutation_refl. - econstructor; eauto. Qed.
imports: Arith List Permutation