proposition: Lemma Mfixvar : (forall (f:A->Distr B), okfun (fun x => Loop (fun y => mu (f y) (q y)) x) (fun x => F f x) q) -> okfun loop (Mfix F) q.
proof: Proof. intros; unfold loop,mufix,fixp. apply okfun_le_compat with (fun x => Ulub (fun n => Ccpo.iter Loop n x)) q; auto. apply fixrule_Ulub with (p:=fun x n => Ccpo.iter Loop n x); simpl; intros;auto. unfold okfun,ok in *|-*. intro x; apply Ole_trans with (2:=H f x). rewrite Loop_eq; apply (mu_monotonic (stop x)); intros. intro b; case b; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)