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