fact: CoInductive semantics_eq {i} : semantics i -> semantics i -> Prop := | semantics_eq_rec (sem sem' : semantics i) (res_eq : forall {a} (e : i a), eval_effect sem e = eval_effect sem' e) (next_eq : forall {a} (e : i a), semantics_eq (exec_effect sem e) (exec_effect sem' e)) : semantics_eq sem sem'.
imports: ExtLib(StateMonad) FreeSpec.Core(ImpureFacts Contract)