Fix performance issue caused by code generation
Writing an unannotated Proxy each time leads the typechecker to construct an exponentially large proof that each Proxy is equal to all the other ones.
It is much kinder of the typechecker to communicate the knowledge that each Proxy must be the same when creating strings by passing the same one as an argument to all builder functions.