fact: Parameter new_defined_object_field : forall (h : t) (p : Program) (cn : ClassName) (um : utsModifier) (fs : FieldSignature) (f : Field) (loc : Object) (h' : t) , new h p (ObjectObject cn um) = Some (loc, h') -> is_defined_field p cn fs f -> get h' (InstanceField loc fs) = Some (init_field_value f).
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)