Automatically created functions:

  ty1_tyn.bn[simp]        lifted equations for bn funs
  ty1_tyn.fv[simp]        lifted equations for fv funs
  ty1_tyn.perm[simp]      lifted permutation equations
  ty1_tyn.distinct[simp]  lifted distincts
  ty1_tyn.eq_iff
  ty1_tyn.induct
  ty1_tyn.inducts
  instance ty1 and tyn :: fs
  ty1_tyn.supp            for too many bindings empty

Smaller things:

- maybe <type>_perm whould be called permute_<type>.simps;
  that would conform with the terminology in Nominal2

- we also need to lift the size function for nominal
  datatypes

Bigger things:

- nested recursion, like types "trm list" in a constructor

- strong induction rules

- check support equations for more bindings per constructor

- automate the proofs that are currently proved with sorry:
  alpha_equivp, fv_rsp, alpha_bn_rsp

- store information about defined nominal datatypes, so that
  it can be used to define new types that depend on these

- make 3 versions of Abs

- make parser aware of bn functions that call other bn functions
  and reflect it in the datastructure passed to Fv/Alpha generation

- make parser aware of recursive and of different versions of abs