proposition: Lemma bindrFree_and_ret {U:choiceType} (mu : Frp_fld U) : bindrFree mu (fun u => retrFree u) = mu.
proof: Proof. unfold bindrFree. induction mu. reflexivity. f_equal. apply boolp.funext. move=> p. specialize (H p). rewrite H. reflexivity. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)