proposition: Lemma valid_package_inject_export : ∀ L I E1 E2 p, fsubset E1 E2 → ValidPackage L I E2 p → ValidPackage L I E1 p.
proof: Proof. intros L I E1 E2 p hE h. apply prove_valid_package. eapply from_valid_package in h. intros o ho. specialize (h o). destruct o as [o [So To]]. forward h. { eapply in_fsubset. all: eauto. } destruct h as [f [ef hf]]. exists f. intuition auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type) Equations.Prop.DepElim Equations(Equations)