proposition: Lemma valid_link : ∀ L1 L2 I M E p1 p2, ValidPackage L1 M E p1 → ValidPackage L2 I M p2 → ValidPackage (L1 :|: L2) I E (link p1 p2).
proof: Proof. intros L1 l2 I M E p1 p2 h1 h2. apply prove_valid_package. eapply from_valid_package in h1. intros [n [So To]] ho. unfold link. rewrite mapmE. specialize (h1 _ ho) as h1'. cbn in h1'. destruct h1' as [f [ef hf]]. rewrite ef. cbn. eexists. split. 1: reflexivity. intro x. eapply valid_code_link. - eapply valid_injectLocations. + apply fsubsetUl. + eapply hf. - eapply valid_package_inject_locations. + apply fsubsetUr. + 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)