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