proposition: Lemma okup_fixrule_inv : forall (p : A -> U) (q : A -> B -> U), (forall (f:A->Distr B), upfun p f q -> upfun p (fun x => F f x) q) -> upfun p (Mfix F) q.
proof: Proof. unfold upfun, okup; intros. unfold Mfix; simpl. apply lub_le. intro n; generalize x; induction n; simpl; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)