fact: Parameter new_typeof : forall (h : t) (p : Program) (lt : ObjectType) (loc : Object) (h' : t) , new h p lt = Some (loc, h') -> typeof h' loc = Some lt.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)