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