1 Smaller things:

     1 Smaller things:

     2 

     2 

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

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

     4   that would conform with the terminology in Nominal2

     4   that would conform with the terminology in Nominal2

     5 

     5 

     6 

     8 

     7 Bigger things:

     9 Bigger things:

     8 

    10 

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

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

    10 

    12