proposition: Lemma valid_trim : ∀ L I E p, ValidPackage L I E p → ValidPackage L I E (trim E p).
proof: Proof. intros L I E p h. apply prove_valid_package. eapply from_valid_package in h. intros [n [So To]] ho. specialize (h _ ho). cbn in h. destruct h as [f [ef hf]]. exists f. intuition auto. apply trim_get. all: 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)