Normal form equality conflicts and uniqueness check (#4497)

Normal form equality conflicts and uniqueness check (#4497)

This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.

It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.