fact: Parameter new_array_no_change : forall (h : t) (p : Program) (length : Int.t) (tp : StaticType) (um : utsModifier) (loc : Object) (h' : t) (am : Location) , new h p (ObjectArray length tp um) = Some (loc, h') -> (forall (i : Int.t) , am <> (ArrayElement loc i)) -> get h' am = get h am.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)