proposition: Lemma instrument_to_state_exec_morphism `{MayProvide ix i} `(c : contract i Ω) `(p : impure ix a) (ω : Ω) : forall (sem : semantics ix), execState (to_state p) sem = execState (runStateT (to_instrument c p) ω) sem.
proof: Proof. unfold execState. revert ω. induction p. + reflexivity. + intros ω sem. cbn -[gen_witness_update]. destruct run_effect; cbn. now rewrite H0 with (ω := gen_witness_update c ω e β0). Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(Contract HoareFacts SemanticsFacts)