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 rulesWhat are the proofs that are still proved by sorry?