proposition: Lemma getm_def_map_dep : ∀ (T : ordType) S1 S2 (l : seq (T * S1)) (f : T → S1 → S2) x, getm_def [seq let '(i,s) := u in (i, f i s) | u <- l ] x = omap (f x) (getm_def l x).
proof: Proof. intros T S1 S2 l f x. induction l as [| u l ih]. - simpl. reflexivity. - simpl. destruct u as [i s]. simpl. destruct (x == i) eqn:e. + cbn. move: e => /eqP e. subst. reflexivity. + apply ih. 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)