Comment changes.
Make an inline version of rules.simplifySite and use it in rules.simplifyStep.
After each user-level proof step try simplifying the result
and showing the simplified version.