The principality of OCaml’s GADT type inference relies on the concept of ambivalence, which allows to reject programs whose typing is ambiguous. Yet, ambivalence itself requires to use a graph view of types, making inductive reasoning more difficult. In this talk, we present our ongoing work on mechanizing the metatheory of a core language for modern OCaml and formally proving soundness and principality for this core language. Our core language supports structural polymorphism, recursive types, and type-level equality witnesses, which are the defining features of OCaml type inference as of version 4.12. We have now proved subject reduction for a meaningful subset of the reduction rules.