--- a/TODO	Fri Feb 04 03:52:38 2011 +0000
+++ b/TODO	Fri Feb 04 04:45:04 2011 +0000
@@ -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