proposition: Lemma run_impure_bind_assoc {i a b} (sem : semantics i) (p : impure i a) (f : a -> impure i b) : run_impure sem (p >>= f) = run_impure (exec_impure sem p) (f (eval_impure sem p)).
proof: Proof. revert sem f. induction p; intros sem g. + reflexivity. + rewrite bind_request_then_assoc. rewrite run_impure_request_then_assoc. rewrite H. rewrite exec_impure_request_then_assoc. rewrite eval_impure_request_then_assoc. reflexivity. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)