proposition: Lemma uniform_unfold {M : probMonad real_realType} (P : rel X) def d : uniform def (enum X) >>= (fun p => Ret (P d p)) = Ret (P d a) <|(/ 3)%coqR%:pr|> (Ret (P d b) <|(/ 2)%coqR%:pr|> Ret (P d c)) :> M _.
proof: Proof. rewrite [LHS](_ : _ = fmap (fun p => P d p) (uniform def (enum X))); last first. by rewrite fmapE; bind_ext; case. by rewrite -(compE (fmap _)) -(uniform_naturality _ true) enumE. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib