--- a/TODO	Mon Jun 20 09:59:18 2011 +0900
+++ b/TODO	Mon Jun 20 10:16:12 2011 +0900
@@ -37,6 +37,9 @@
 - nominal_induct cannot avoid a term (for example function applied
   to an argument).
 
+- .induct and .exhaust could be the default methods for induction/cases
+  on nominal datatypes
+
 Other:
 
 - nested recursion, like types "trm list" in a constructor