Right. I implemented the second transform. It took some pondering but, as it turned out, it wasn't hard once I got the invariants, there were little, right. Because I dumbed down the language, the pass only needs to collect the quantified variables it encounters in a local state, determine new record declarations at each record statement rewrite, and pass the new constructed declarations to the top level.
The subsequent implementation of the pass is somewhat verbose, but somewhere much simpler than in the bootstrap. Just a class which implements a rewrite and has as local state a variable list and a set of declarations. I didn't need the nested context yet.
I am inclined to say that imperative wins but I am near certain the pass in the bootstrap can be rewritten more concisely. Must have been due to trying to use the transform function I had just invented, the changes I made during the development, and the more elaborate type system I was unsure I would, or could, support at the time of writing.