proposition: Lemma compliant_semantics_caller_obligation_compliant `{MayProvide ix i} {Ω α} (c : contract i Ω) (ω : Ω) (e : ix α) (o_caller : gen_caller_obligation c ω e) (sem : semantics ix) (comp : compliant_semantics c ω sem) : compliant_semantics c (gen_witness_update c ω e (eval_effect sem e)) (exec_effect sem e).
proof: Proof. inversion comp; ssubst. now apply next. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)