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