proposition: Lemma hide_pick_nondeter : (do h <- hide_n; do p <- pick def : M _; Ret (h == p) = uFFT)%Do.
proof: Proof. transitivity (fmap (uncurry (fun a b => a == b)) (do h <- hide_n; do p <- pick def : M _; Ret (h, p)))%Do. rewrite fmapE !bindA; bind_ext => y1. by rewrite !bindA; under [RHS]eq_bind do rewrite bindretf. rewrite monty_choice_your_choice_combine -!/(try _). by rewrite 2!alt_fmapDr !try_uFFT 2!altmm. 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