proposition: Lemma removeFirst_in_iff : forall (A : Set)(eqd : eq_dec A)(ls : list A) a1 a2, In a1 (removeFirst eqd ls a2) -> In a1 ls.
proof: Proof. induction ls; intuition; simpl in *. destruct (eqd a2 a); subst. intuition. simpl in *. intuition. right. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool