proposition: Lemma permutation_remove {A} eq_dec (a : A) l l' : Permutation (a :: l) l' -> Permutation l (remove1 eq_dec a l').
proof: Proof. remember (a :: l) as al. intros HP. revert a l Heqal. induction HP; intros a L EL. - inversion EL. - inversion EL; subst. simpl. destruct (eq_dec a a). auto. tauto. - inversion EL; subst. simpl. destruct (eq_dec a _). subst. constructor. apply Permutation_refl. constructor. destruct (eq_dec a a). auto. tauto. - apply perm_trans with (remove1 eq_dec a l'). apply (IHHP1 a L EL). apply permutation_remove1. auto. Qed.
imports: Arith List Permutation