proposition: Lemma code_link_bind : ∀ {A B : choiceType} (v : raw_code A) (k : A → raw_code B) (p : raw_package), code_link (bind v k) p = bind (code_link v p) (λ x, code_link (k x) p).
proof: Proof. intros A B v k p. induction v. - cbn. reflexivity. - cbn. destruct lookup_op. + rewrite bind_assoc. f_equal. apply functional_extensionality. auto. + eauto. - cbn. f_equal. apply functional_extensionality. auto. - cbn. f_equal. auto. - cbn. f_equal. apply functional_extensionality. auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)