proposition: Lemma cover_orc_0_1 : forall (A:Type)(P:set A)(f:MF A), cover P f -> forall x, orc (f x == 0) (f x == 1).
proof: Proof. intros; apply (excluded_middle (A:=P x)); intros; auto. apply orc_right; apply cover_eq_one with (P:=P) (f:=f); auto. apply orc_left; apply cover_eq_zero with (P:=P) (f:=f); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)