proposition: Lemma valid_package_inject_locations : ∀ I E L1 L2 p, fsubset L1 L2 → ValidPackage L1 I E p → ValidPackage L2 I E p.
proof: Proof. intros I E L1 L2 p hL h. apply prove_valid_package. eapply from_valid_package in h. intros [n [S T]] ho. specialize (h _ ho). cbn in h. destruct h as [f [ef hf]]. exists f. intuition auto. eapply valid_injectLocations. all: eauto. 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)