proposition: Lemma trim_get : ∀ E (p : raw_package) n So To f, p n = Some (So ; To ; f) → (n, (So, To)) \in E → trim E p n = Some (So ; To ; f).
proof: Proof. intros E p n So To f e h. unfold trim. rewrite filtermE. rewrite e. cbn. rewrite h. 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)