Smaller things:- case names for "weak" induction rules (names of the constructors); see page 61/62 and 170 in Tutorial- <type>_perm rules should be added to the simplifier; maybe <type>_perm whould be called permute_<type>.simps; that would conform with the terminology in Nominal2- <type>_fv / <type>_bn / <type>_distinct should also be added to the simplifierBigger 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