Yes, you should comment out PrintT for proofs. Since PrintT is evaluated only for its side effect, expanding the definition would probably be harmless. But this is not the case for other operators defined in the TLC module. For example, TLC evaluates x \in Any to TRUE, for any x, but this could not be proved based on the definition of Any and even worse, adding the axiom "\A x : x \in Any" would make the logic of TLA+ inconsistent. (It is harmless for finite domains that TLC is based on.)
But you are raising an interesting question. We should probably reconsider which operators could and should be supported in proofs.
Regards,
Stephan