proposition: Lemma outOfFree_vs_callrFree : forall op : sigma_ops, outOfFree sigMap _ (callrFree _ _ op) = sigMap op.
proof: Proof. move=> op. cbn. epose (T_bindRet := ord_relmon_law1 T _). eapply FunctionalExtensionality.equal_f in T_bindRet. cbn in T_bindRet. erewrite T_bindRet. reflexivity. Qed.
imports: Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Mon(SPropBase) mathcomp(all_ssreflect) Crypt(FreeProbProg ChoiceAsOrd)