So all the complicated logic is in program 1
Indeed. You will, of course, write a specification of the two translations for others to examine. I think you will find it to be an interesting exercise. The Toolbox's Decompose Proof command has to solve the problem of maintaining indentation while expanding definitions in a proof step. It works right most of the time, but it's not perfect. Program 1 will have to be perfect if people are to trust it.