--- a/TODO	Thu Mar 25 14:31:51 2010 +0100
+++ b/TODO	Thu Mar 25 15:06:58 2010 +0100
@@ -22,19 +22,21 @@
 
 - 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
 
 - check support equations for more bindings per constructor
 
-- automate the proofs that are currently proved with sorry:
-  alpha_equivp
+- For binding functions that call other binding functions
+  the following are proved with cheat_tac:
+    bn_eqvt, bn_rsp, alpha_bn_rsp, constr_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these
 
-- make parser aware of bn functions that call other bn functions
-  and reflect it in the datastructure passed to Fv/Alpha generation
-
 - make parser aware of recursive and of different versions of abs
 
 Less important: