proposition: Lemma eval_impure_bind_assoc {i a b} (sem : semantics i) (p : impure i a) (f : a -> impure i b) : eval_impure sem (p >>= f) = eval_impure (exec_impure sem p) (f (eval_impure sem p)).
proof: Proof. unfold eval_impure. now rewrite run_impure_bind_assoc. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)