--- a/TODO	Sat Mar 20 16:27:51 2010 +0100
+++ b/TODO	Sat Mar 20 18:16:26 2010 +0100
@@ -24,10 +24,10 @@
 
 - strong induction rules
 
-- show support equations
+- check support equations for more bindings per constructor
 
 - automate the proofs that are currently proved with sorry:
-  alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
+  alpha_equivp, fv_rsp, alpha_bn_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these