proposition: Lemma in_getm_def_None : ∀ {A : eqType} n (x : A) (s : seq (nat * A)), (n,x) \in s → getm_def s n = None → False.
proof: Proof. intros A n x s h1 h2. induction s as [| [m a] s ih] in n, x, h1, h2 |- *. - inversion h1. - cbn in h2. rewrite in_cons in h1. destruct eqn eqn:e. + discriminate. + cbn in h1. rewrite e in h1. cbn in h1. eapply ih. all: eauto. 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)