proposition: Lemma valid_code_link : ∀ A L Im Ir (v : raw_code A) p, ValidCode L Im v → ValidPackage L Ir Im p → ValidCode L Ir (code_link v p).
proof: Proof. intros A L Im Ir v p hv hp. induction hv. all: try solve [ constructor ; auto ]. eapply lookup_op_valid in hp as hf. 2: eauto. destruct hf as [f [ef hf]]. cbn. rewrite ef. apply valid_bind. all: 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)