proposition: Lemma valid_par_upto : ∀ L I E L1 L2 I1 I2 E1 E2 p1 p2, Parable p1 p2 → ValidPackage L1 I1 E1 p1 → ValidPackage L2 I2 E2 p2 → fsubset (L1 :|: L2) L → fsubset (I1 :|: I2) I → fsubset E (E1 :|: E2) → ValidPackage L I E (par p1 p2).
proof: Proof. intros L I E L1 L2 I1 I2 E1 E2 p1 p2 h h1 h2 hL hI hE. eapply valid_package_inject_locations. 1: eauto. eapply valid_package_inject_import. 1: eauto. eapply valid_package_inject_export. 1: eauto. eapply valid_par. all: eauto. 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)