A Metatheory of a Mechanized Object Theory