Type checking algorithms for the Hindley-Damas-Milner type system (HDM) have been the subject of much research. Specifically, such algorithms have been proven sound, complete, and decidable, and some of these proofs have been mechanized. Yet, elaboration algorithms which (in addition to verifying the well-typedness of programs) convert programs from HDM into richer and more precise calculi – such as System F – have received much less attention. We motivate analyzing elaboration algorithms to the same level of detail, and present our ongoing work towards mechanizing an algorithm which elaborates terms from HDM to System F.