--- a/TODO	Sat Feb 05 07:38:22 2011 +0900
+++ b/TODO	Sat Feb 05 07:39:00 2011 +0900
@@ -1,3 +1,7 @@
+Function definitions
+
+- export proofs bout alpha_bn
+
 
 Parser should check that:
 
@@ -16,12 +20,6 @@
 
 - nested recursion, like types "trm list" in a constructor
 
-- define permute_bn automatically and prove properties of it
-
-- prove renaming-of-binders lemmas
-
-- strong induction rules
-
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these