fact: Parameter new_undefined_object_field : forall (h : t) (p : Program) (cn : ClassName) (um : utsModifier) (fs : FieldSignature) (loc : Object) (h' : t), new h p (ObjectObject cn um) = Some (loc, h') -> ~ defined_field p cn fs -> get h' (InstanceField loc fs) = None.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)