proposition: Lemma lookup_op_unionm : ∀ p1 p2 o, lookup_op (unionm p1 p2) o = if isSome (p1 (fst o)) then lookup_op p1 o else lookup_op p2 o.
proof: Proof. intros p1 p2 [n [So To]]. cbn. rewrite unionmE. destruct (p1 n) as [[S1 [T1 f1]]|] eqn:e1. all: 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)