Smaller things:- maybe <type>_perm whould be called permute_<type>.simps; that would conform with the terminology in Nominal2Bigger things:- nested recursion, like types "trm list" in a constructor- strong induction rules- show support equations- automate the proofs that are currently proved with sorry: alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp- store information about defined nominal datatypes, so that it can be used to define new types that depend on these- make 3 versions of Abs- make parser aware of bn functions that call other bn functions and reflect it in the datastructure passed to Fv/Alpha generation- make parser aware of recursive and of different versions of abs