proposition: Lemma cover_esp_mult_left : forall (A:Type)(P:set A)(f:MF A)(p:U), cover P f -> forall x, f x & p == f x * p.
proof: Proof. intros; apply Uesp_zero_one_mult_left. apply (cover_orc_0_1 H x). Qed.
imports: ALEA(Utheory) ALEA(Sets)