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