Display matched rules in more proof paths

[FullyNonlinear]

Currently, the names of the matched rules are displayed in certain paths, prominently when there is an error or constraints are produced. This PR displays the names of the rules whenever a rule is matched. The benefit is that the rules picked are easily identified when debugging, even when the test case does not expect a failure. From experience, I find it particularly helpful for beginners to this project.