proposition: Lemma fconj_zero_one : forall (A:Type)(f g:MF A), zero_one f -> zero_one g -> zero_one (fconj f g).
proof: Proof. red; unfold fconj; intros; apply (H x); intros. auto. apply orc_left. rewrite H1; auto. apply (H0 x); intros. auto. apply orc_left. rewrite H2; auto. apply orc_right. rewrite H1; rewrite H2; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)