fact: Definition CorrespondingState (p : Program) (st_rac : State.t) (st_sem : Sem.State.t) : Prop := st_sem@h %sem = st_rac@h /\ CorrespondingFrame p st_rac@fr st_sem@fr %sem.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)