proposition: Lemma trim_get_inv : ∀ E p n So To f, trim E p n = Some (So ; To ; f) → p n = Some (So ; To ; f) ∧ (n, (So, To)) \in E.
proof: Proof. intros E p n So To f e. unfold trim in e. rewrite filtermE in e. cbn in e. destruct (p n) as [[S1 [T1 f1]]|] eqn:e1. 2:{ rewrite e1 in e. cbn in e. discriminate. } rewrite e1 in e. cbn in e. destruct ((n, (S1, T1)) \in E) eqn:e2. 2:{ rewrite e2 in e. discriminate. } rewrite e2 in e. noconf e. intuition 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)