proposition: Lemma link_assoc : ∀ p1 p2 p3, link p1 (link p2 p3) = link (link p1 p2) p3.
proof: Proof. intros p1 p2 p3. apply eq_fmap. unfold link. intro n. repeat rewrite ?mapmE. destruct (p1 n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity. cbn. f_equal. f_equal. f_equal. extensionality x. rewrite code_link_assoc. reflexivity. 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)