proposition: Lemma ntherrorP (T : ml_type) (e : Env) (r : loc T) : nth_error_spec e r.
proof: Proof. case H : (nth_error e (loc_id r)) => [[T' s']|]. have [Ts'|Ts'] := boolP (coercible T s'). have ? := coercible_eq Ts'; subst T'. exact: NthError H. exact: NthError_nocoerce H Ts'. exact: NthError_None. Qed.
imports: JMeq mathcomp(all_ssreflect) mathcomp(finmap) mathcomp(classical_sets) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer