1 Smaller things:

     2 

     3 - case names for "weak" induction rules (names of the 

     4 constructors); see page 61/62 and 170 in Tutorial

     5 

     6 - <type>_perm rules should be added to the simplifier;

     7   maybe <type>_perm whould be called permute_<type>.simps;

     8   that would conform with the terminology in Nominal2

     9 

    10 - <type>_fv / <type>_bn / <type>_distinct should also be 

    11   added to the simplifier

    12 

    13 

    14 Bigger things:

    15 

    16 - nested recursion, like types "trm list" in a constructor

    17 

    18 - strong induction rules

    19 

    20 

    21 What are the proofs that are still proved by sorry?