fact: Definition ValidStoreRefs (p : Program) (c : Class) (m : Method) (st : State.t) : StoreRefList := let sr_list := ExtractAssignableClauses (ValidCase p c m st) in if AssignableEverything sr_list then \everything else if AssignableNothing sr_list then \nothing else StoreRefs (ConcatinateStoreRefs sr_list).
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)