tuned;

removes some unused code that used to try to derive a simpler version of the eqvt lemmas

Adapted to new inductive definition package.

clarified code

- Replaced fold by fold_rev to make sure that list of predicate variables pvars (for invariants) is in the correct order - Adapted to new format of datatype descriptor

- Changed format of descriptor contained in nominal_datatype_info - Equivariance proof for graph of primrec combinator no longer uses large simpset (more robust).