proposition: Lemma valid_link_upto : ∀ L1 L2 L I M E p1 p2, ValidPackage L1 M E p1 → ValidPackage L2 I M p2 → fsubset L1 L → fsubset L2 L → ValidPackage L I E (link p1 p2).
proof: Proof. intros L1 L2 L I M E p1 p2 h1 h2 hL1 hL2. eapply valid_package_inject_locations. 2: eapply valid_link. 2-3: eauto. rewrite fsubUset. rewrite hL1 hL2. 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)