Finished formalizing the translation, but I am quite stuck on how to formalize the typing rules I have set up on paper for the intermediate structures I wound up using. Grr.