To extend the formalization of type inference with various practical features, including bounded quantification and union and intersection types, a minimal, unified and scalable metatheory is firstly needed. In this talk, I will introduce my current work on simplifying type inference and show how the proofs are simplified in this approach.