proposition: Lemma trimmed_valid_Some_in : ∀ L I E p n S T f, ValidPackage L I E p → trimmed E p → p n = Some (S ; T ; f) → (n, (S, T)) \in E.
proof: Proof. intros L I E p n S T f hv ht e. unfold trimmed in ht. pose e as e'. rewrite <- ht in e'. unfold trim in e'. rewrite filtermE in e'. rewrite e in e'. simpl in e'. destruct ((n, (S, T)) \in E) eqn:e2. 2:{ rewrite e2 in e'. discriminate. } 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)