proposition: Lemma getm_def_in : ∀ {A : eqType} n (x : A) (s : seq (nat_eqType * A)), getm_def s n = Some x → (n,x) \in s.
proof: Proof. simpl. intros A n x s h. induction s as [| [m a] s ih] in n, x, h |- *. - inversion h. - cbn in h. rewrite in_cons. apply/orP. destruct eqn eqn:e. + noconf h. move: e => /eqP e. subst. left. apply/eqP. reflexivity. + right. eapply ih. 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)