4.1. Congruence closure
Whenever there is a function f in the context, grind will equate f a₁ ... aₙ and f b₁ ... bₙ whenever a₁ = bₙ, ..., aₙ = bₙ.
It does this always when there is something new to add.
Whenever there is a function f in the context, grind will equate f a₁ ... aₙ and f b₁ ... bₙ whenever a₁ = bₙ, ..., aₙ = bₙ.
It does this always when there is something new to add.