proposition: Lemma lookup_op_trim : ∀ E o p, lookup_op (trim E p) o = obind (λ f, if o \in E then Some f else None) (lookup_op p o).
proof: Proof. intros E [n [So To]] p. unfold lookup_op, trim. rewrite filtermE. destruct (p n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity. cbn. destruct ((n, (S1, T1)) \in E) eqn:e1. - rewrite e1. destruct choice_type_eqP. 2: reflexivity. destruct choice_type_eqP. 2: reflexivity. cbn. subst. cbn. rewrite e1. reflexivity. - rewrite e1. destruct choice_type_eqP. 2: reflexivity. destruct choice_type_eqP. 2: reflexivity. subst. rewrite e1. cbn. 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)