- When the encoding can't encode a definition it transform it into an
   axiom. But it's not the same than before. The differences is that
   eliminate algebraic is before this transformation into axiom and
   not after. So if the definition start with a match, in one case
   that give different nice axioms, and in the other case that
   introduce a match function which is polymorph and not well used by
   provers.

   Possible solutions :
   1) make the match function easier to use with some modification to
   its definition and discriminate it.
   2) Eliminate the match function when the encoding tranform a
   definition into axioms.

This reverts commit 1f652980.