proposition: Lemma run_impure_equation {i a} (sem : semantics i) (p : impure i a) : run_impure sem p = (eval_impure sem p, exec_impure sem p).
proof: Proof. unfold eval_impure, exec_impure. destruct run_impure; reflexivity. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)