proposition: Lemma removeFirst_permutation : forall (A : Set)(eqd : eq_dec A)(ls : list A) a, In a ls -> Permutation ls (a :: (removeFirst eqd ls a)).
proof: Proof. induction ls; intuition; simpl in *; intuition; subst. destruct (eqd a0 a0); try congruence. eapply Permutation_refl. destruct (eqd a0 a); subst. eapply Permutation_refl. eapply perm_trans; [idtac | eapply perm_swap]. eapply perm_skip. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool