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?+
−