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.