proposition: Lemma cover_eq_one_elim : forall (A:Type)(P:set A)(f:MF A), cover P f -> forall z, f z == 1 -> ~ ~ P z.
proof: Proof. intros. apply (cover_eq_one_elim_class (Q:=fun z => ~ ~ P z) H); auto. red; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)