proposition: Lemma bind_cmd_bind : ∀ {A B C : choiceType} (c : command A) (k1 : _ → raw_code B) (k2 : _ → raw_code C), bind (cmd_bind c k1) k2 = cmd_bind c (λ x, bind (k1 x) k2).
proof: Proof. intros A B C c k1 k2. destruct c. all: simpl. all: reflexivity. 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)