proposition: Lemma bind_cnew T (s : coq_type T) A (k : loc T -> M A) e : (cnew s >>= k) e = k (fresh_loc T e) (extend_env s e).
proof: Proof. by case: e. Qed.
imports: JMeq mathcomp(all_ssreflect finmap) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer monad_model