proposition: Lemma to_hoare_step `{MayProvide ix i} `(c : contract i Ω) `(e : ix a) `(f : a -> impure ix a) `(hpre : pre (to_hoare c (request_then e f)) ω) (x : a) (step : gen_callee_obligation c ω e x) : pre (to_hoare c (f x)) (gen_witness_update c ω e x).
proof: Proof. destruct hpre as [hbefore hafter]. apply hafter. cbn. unfold gen_callee_obligation, gen_witness_update in *. now destruct proj_p. Qed.
imports: FreeSpec.Core(Interface ImpureFacts Contract)