proposition: Lemma no_contract_compliant_semantics `{MayProvide ix i} (sem : semantics ix) (u : unit) : compliant_semantics (no_contract i) u sem.
proof: Proof. revert sem. cofix no_contract_compliant_semantics; intros sem. constructor. + intros α e req. unfold gen_caller_obligation, gen_callee_obligation. destruct proj_p; constructor. + intros α e req. unfold gen_witness_update. destruct (proj_p e); [ apply no_contract_compliant_semantics | auto with freespec ]. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)