Function definitions

- export proofs bout alpha_bn
- equations like

    | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"

  do not work

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 <type>_perm whould be called permute_<type>.simps;
  that would conform with the terminology in Nominal2


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