--- a/TODO	Fri Mar 26 10:07:26 2010 +0100
+++ b/TODO	Fri Mar 26 10:35:26 2010 +0100
@@ -31,8 +31,7 @@
 - check support equations for more bindings per constructor
 
 - For binding functions that call other binding functions
-  the following are proved with cheat_tac:
-    bn_eqvt, bn_rsp, alpha_bn_rsp, constr_rsp
+  the following are proved with cheat_tac: constr_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these