fact: Definition LocInObjSet (loc : Location) (objs : ObjSet.t) : bool := match loc with | Heap.InstanceField obj _ | Heap.ArrayElement obj _ => ObjSet.mem obj objs | _ => false end.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)