Smaller things:

- case names for "weak" induction rules (names of the 

constructors); see page 61/62 and 170 in Tutorial

- maybe <type>_perm whould be called permute_<type>.simps;

  that would conform with the terminology in Nominal2

Bigger things:

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

- strong induction rules

- show support equations

- automate the proofs that are currently proved with sorry:

  alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp

- 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