proposition: Lemma get_op_default_link : ∀ p q o x, get_op_default (p ∘ q) o x = code_link (get_op_default p o x) q.
proof: Proof. intros p q o x. unfold get_op_default. rewrite lookup_op_link. destruct lookup_op as [f|] eqn:e. 2: reflexivity. simpl. reflexivity. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)