fact: Definition stT_thetaDens := rlmm_from_lmla stT_thetaDens_adj.
imports: Coq(RelationClasses) Mon(SPropBase) mathcomp(all_ssreflect) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples TransformingLaxMorph SubDistr Theta_dens LaxFunctorsAndTransf UniversalFreeMap FreeProbProg StateTransformingLaxMorph LaxComp)