`"lab" 0 = 0' means `"lab" (0 = 0)', so adding a typecast to lhs
must not change the binding

This reverts commit 9809329892bb9637a0137d330ecd08a16ede2d93.

This reverts commit 70a9e16d1d5818186692ca50931712e1fe2f19f0.

This reverts commit c3b4196fd737315a9328f5729c839a18f709b471.

The relevant hash-tables are weak both in keys and values

encoding_enumeration add projection for enumerated type. Seems to work (on valid and not valid goal) for simplify, spass, eprover

see examples/programs/sorted_list.mlw with eprover, spass, simplify!!

encoding_enumeration must be used with encoding_decorate and encoding_instantiate if an enumeration type is kept.

This allows to have one line less in transformations.

with a different logic of splitting in premises - to discuss.
Its main advantage is providing two transformations instead of 6.

a meta of an exclusive kind removes the previous meta of this 
kind (if any) from task_meta.

Discuss: should driver-imposed exclusive metas have a low priority
(i.e. driver does not add an exclusive meta if the task already 
contains one of this kind) or should we just trust the driver
authors not to put exclusive metas in drivers? 

- bring driver syntax closer to that of theories
- some simple API improvements