Print error messages with more hidden information based on α-equivalence .

The comparison on terms which triggers new printing flags in case two terms which are different would be printed identically now contains α-equivalence.

The implementation using a canonization function on [constr] instead of trying to deal with [constr_expr] was suggested by Hugo.