simpIf methods. It contains all congruence theorems, but
just the rewriting rules for reducing
discharge? function for
It only uses hypotheses from the local context. It is effective
after a case-split.
- One or more equations did not get rendered due to their size.