[bvssvni]

Yeah, this is too imprecise. I tried to translate to your terminology, but failed.

My system uses "tautological equality" and this allows me to treat them the save way for all tautological congruent operators. Ofc, you can't treat them the same if an operator is neither normal nor tautological congruent.

Even if you have a such operator `foo'(x)` you can prove `foo'(x)`, `(foo'(x) == foo'(x))^true` or `foo'(x) == foo'(x)` etc. If this is what you are talking about, then this system supports it.