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 infrastructureNominal_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 typeSmaller 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 datatypesOther:- 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