Automatically created functions: ty1_tyn.bn[simp] lifted equations for bn funs ty1_tyn.fv[simp] lifted equations for fv funs ty1_tyn.perm[simp] lifted permutation equations ty1_tyn.distinct[simp] lifted distincts ty1_tyn.eq_iff ty1_tyn.induct ty1_tyn.inducts instance ty1 and tyn :: fs ty1_tyn.supp for too many bindings emptySmaller things:- maybe <type>_perm whould be called permute_<type>.simps; that would conform with the terminology in Nominal2- we also need to lift the size function for nominal datatypesBigger things:- nested recursion, like types "trm list" in a constructor- strong induction rules- check support equations for more bindings per constructor- automate the proofs that are currently proved with sorry: alpha_equivp, fv_rsp, alpha_bn_rsp- 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