Function definitions- export proofs bout alpha_bnParser 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 typeSmaller things:- maybe <type>_perm whould be called permute_<type>.simps; that would conform with the terminology in Nominal2Other:- 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