proposition: Lemma removeFirst_NoDup : forall (A : Set)(eqd : eq_dec A)(ls : list A) a, NoDup ls -> NoDup (removeFirst eqd ls a).
proof: Proof. induction ls; intuition; simpl in *. inversion H; clear H; subst. destruct (eqd a0 a); subst. trivial. econstructor. eapply removeFirst_not_in. intuition. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool