fact: Definition EquivAssignableHeap (p : Program) (h h' : Heap.t) (pivots : LocSet.t) : Prop := forall loc, PivotField p loc -> ~ LocSet.In loc pivots -> Heap.get h loc = Heap.get h' loc.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)