fact: Definition appLocations (l1 l2:StoreRefList) : StoreRefList := match l1, l2 with | Nothing, _ | _, Everything => l2 | Everything, _ | _, Nothing => l1 | StoreRefs s1, StoreRefs s2 => StoreRefs (List.app s1 s2) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)