proposition: Lemma bind_ret : ∀ A (v : raw_code A), bind v (λ x, ret x) = v.
proof: Proof. intros A v. induction v. all: cbn. 1: reflexivity. all: try solve [ f_equal ; apply functional_extensionality ; eauto ]. f_equal. auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type) Equations.Prop.DepElim Equations(Equations)