proposition: Lemma run_impure_request_then_assoc {i a b} (sem : semantics i) (e : i a) (f : a -> impure i b) : run_impure sem (request_then e f) = run_impure (exec_effect sem e) (f (eval_effect sem e)).
proof: Proof. cbn; now rewrite run_effect_equation. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)