proposition: Lemma code_link_if : ∀ A (c₀ c₁ : raw_code A) (p : raw_package) b, code_link (if b then c₀ else c₁) p = if b then code_link c₀ p else code_link c₁ p.
proof: Proof. intros A c₀ c₁ p b. destruct b. all: 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)