--- a/TODO	Mon Mar 22 15:27:01 2010 +0100
+++ b/TODO	Mon Mar 22 17:21:27 2010 +0100
@@ -27,7 +27,7 @@
 - check support equations for more bindings per constructor
 
 - automate the proofs that are currently proved with sorry:
-  alpha_equivp, alpha_bn_rsp
+  alpha_equivp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these