A metatheory of a mechanized object theory