proposition: Lemma getm_def_map_interface_None : ∀ A (I : seq opsig) (f : ∀ x, x \in I → A) n, getm_def [interface (ide x, f x h) | h # x ∈ I] n = None → getm_def I n = None.
proof: Proof. cbn. intros A I f n e. induction I in f, n, e |- *. - simp map_interface in e. auto. - simp map_interface in e. cbn in e. destruct eqn eqn:e1. 1: discriminate. cbn. rewrite e1. specialize IHI with (1 := e). auto. 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)