proposition: Lemma lookup_op_ID : ∀ I o, flat I → lookup_op (ID I) o = if o \in I then Some (λ x, opr o x (λ y, ret y)) else None.
proof: Proof. intros I [n [S T]] h. unfold lookup_op. rewrite IDE. destruct getm_def as [[So To]|] eqn:e. - cbn. apply getm_def_in in e as h1. destruct choice_type_eqP. 2:{ destruct ((n, (S, T)) \in I) eqn:e1. 2:{ rewrite e1. reflexivity. } specialize (h _ _ _ h1 e1). noconf h. congruence. } destruct choice_type_eqP. 2:{ destruct ((n, (S, T)) \in I) eqn:e1. 2:{ rewrite e1. reflexivity. } specialize (h _ _ _ h1 e1). noconf h. congruence. } subst. rewrite h1. reflexivity. - cbn. destruct ((n, (S, T)) \in I) eqn:e1. 1:{ exfalso. eapply in_getm_def_None. 2: eauto. exact e1. } rewrite e1. 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)