Function definitions

- nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?

- nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]

- equations that talk about True/False, for example
    | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
  do not work (since 'function' does not work)

- equivariance for functions can be derived automatically (knowing termination and
  equivariance of the graph).

- for multiple simultanously defined functions, compatibility cases should fold the
  definition and derive eqvt_at for the folded one

- equivariance of the graph for multiple functions does not use equivariance
  infrastructure

Nominal_Datatype Parser should check that:

- types of bindings match types of binding functions
- fsets are not bound in lst bindings
- bound arguments are not datatypes
- binder is referred to by name and not by type

Smaller things:

- maybe <t1_t2>.perm_simps should be called permute_<type>.simps;
  that would conform with the terminology in Nominal2

- nominal_induct does not work without an induction rule

- nominal_induct throws strange "THM" exceptions if not enough
  variables are given

- nominal_induct cannot avoid a term (for example function applied
  to an argument).

- .induct and .exhaust could be the default methods for induction/cases
  on nominal datatypes

Other:

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

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