proposition: Lemma cnewgetD_helper e T T' r v (s : coq_type T') A (k : loc T' -> coq_type T -> M A) : nth_error (ofEnv e) (loc_id r) = Some (mkbind v) -> (cnew s >>= (fun r' => cget r >>= k r')) e = (cnew s >>= (fun r => k r v)) e.
proof: Proof. move=> H. rewrite bind_cnew//. by rewrite (Some_cget v) // (nth_error_rcons_some _ H). Qed.
imports: JMeq mathcomp(all_ssreflect finmap) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer monad_model