proposition: Lemma fesp_conj_zero_one : forall (A:Type)(f g:MF A), zero_one f -> fesp f g == fconj f g.
proof: Proof. unfold fesp,fconj; intros; simpl; apply ford_eq_intro; intro x; apply Uesp_zero_one_mult_left; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)