proposition: Lemma run_effect_equation {i α} (sem : semantics i) (e : i α) : run_effect sem e = (eval_effect sem e, exec_effect sem e).
proof: Proof. unfold eval_effect, exec_effect. destruct run_effect; reflexivity. Qed.
imports: Coq(Program Setoid Morphisms) ExtLib(Monad StateMonad)