proposition: Lemma bind_assoc : ∀ {A B C : choiceType} (v : raw_code A) (k1 : A → raw_code B) (k2 : B → raw_code C), bind (bind v k1) k2 = bind v (λ x, bind (k1 x) k2).
proof: Proof. intros A B C v k1 k2. induction v in k1, k2 |- *. - cbn. reflexivity. - cbn. f_equal. apply functional_extensionality. auto. - cbn. f_equal. extensionality z. auto. - cbn. f_equal. auto. - cbn. f_equal. extensionality z. 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)