It was used in a few places to represent complementary literals,
but is mostly used to represent vectors of terms, variables.  This
commit removes the usage for complementary literals.  The few
places that used it now define the complement manually.

Also introduces the notation of $\bar x_n$ which is used in several places.

It's n-ary.

This was a copy past error from the definition of eq_congruent.
The special "power" of eq_congruent_preg is the additional negation

Caught by Bruno