proposition: Lemma FilterLIn : forall {A: Type} (f: A -> bool), forall x l, LIn x (filter f l) <=> LIn x l # f x = true.
proof: Proof. induction l; simpl. dintuition. intros. case_eq (f a); intros; simpl; dintuition congruence. Qed.
imports: UsefulTypes bin_rels Omega