Clear rewrite rule for Regression testing
Add supporting precondition for lemmas, change some test cases with new rewriter