Prove Admitted theorems in types.ObjectClassifier

They are not very pretty, but they are no longer admits.  This is
partial work on #195.