Alternative treatment of conditional equalities/equivalences should be investigated.
Currently, conditions are converted into Mathematica conditions on the rewrite rules.
A maybe better way of dealing with conditions would be to ignore them in the rewrite rules but add new proof branches in order to prove the conditions before or later.
Proving the conditions would be certainly more powerful than just checking them by computation.
Question: How to deal with multiple rewrite possibilities? Use ReplaceList and produce alternatives?
Alternative treatment of conditional equalities/equivalences should be investigated.