proposition: Lemma store_complies_to_store_specs {s} (st : s) : compliant_semantics (store_specs s) st (store st).
proof: Proof. revert st; cofix compliant_semantics_rec; intros st. constructor. + intros a [| st'] _. ++ now constructor. ++ now constructor. + intros a e req. cbn. replace (exec_effect (store st) e) with (store (store_update s st a e (eval_effect (store st) e))) by now destruct e as [| st']. apply compliant_semantics_rec. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)