proposition: Lemma lookup_op_map : ∀ p o f, lookup_op (@mapm _ typed_raw_function _ (λ '(So ; To ; g), (So ; To ; f So To g)) p) o = omap (f (chsrc o) (chtgt o)) (lookup_op p o).
proof: Proof. intros p [n [So To]] f. unfold lookup_op. rewrite mapmE. destruct (p n) as [[St [Tt ft]]|] eqn:e. 2:{ cbn. reflexivity. } cbn. destruct choice_type_eqP. 2: reflexivity. destruct choice_type_eqP. 2: reflexivity. cbn. subst. 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)