proposition: Lemma code_link_assoc : ∀ A (v : raw_code A) f g, code_link (code_link v f) g = code_link v (link f g).
proof: Proof. intros A v f g. induction v in f, g |- *. - cbn. reflexivity. - cbn. unfold link in *. rewrite lookup_op_map. destruct lookup_op eqn:e. + cbn. rewrite code_link_bind. f_equal. apply functional_extensionality. auto. + cbn. 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)