proposition: Lemma Mfix_eq : forall (A B:Type) (F: (A -O-> cDistr B) -m> A -O-> cDistr B), continuous F -> forall (x :A), Mfix F x == F (Mfix F) x.
proof: Proof. intros; unfold Mfix; apply ford_eq_elim with (n:=x). apply (fixp_eq H). Qed.
imports: ALEA(Monads) ALEA(Utheory)