proposition: Lemma ne_all_not_in : forall (A : Type)(ls : list A) a, (forall a', In a' ls -> a <> a') -> ~In a ls.
proof: Proof. induction ls; intuition; simpl in *. intuition; subst. eapply H; eauto. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation