Michelson: remove the 'ty_value' definition for temporary simplification

I think the simplest, for now, is to remove the ty_value type. Thus the definition of conversion from ty to Set is invalid when we consider values in the Coq AST, because then the conversion of the type for "lambda" for example is:

Script_typed_ir.lambda

rather than:

With_family.lambda arg reg

But we can do the update later, and with this version, we can already cover everything except the instructions handling lambdas or contracts, for which we will not be able to do the proof for now.