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 simplifier


Bigger things:

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

- strong induction rules


What are the proofs that are still proved by sorry?