--- a/TODO	Mon Mar 22 10:15:46 2010 +0100
+++ b/TODO	Mon Mar 22 14:07:07 2010 +0100
@@ -8,7 +8,7 @@
   ty1_tyn.induct
   ty1_tyn.inducts
   instance ty1 and tyn :: fs
-  ty1_tyn.supp            for too many bindings empty
+  ty1_tyn.supp            empty when for too many bindings
 
 Smaller things:
 
@@ -27,14 +27,17 @@
 - 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_equivp, alpha_bn_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these
 
-- make 3 versions of Abs
-
 - 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:
+
+- fv_rsp uses 'blast' to show goals of the type:
+  a u b = c u d   ==>  a u x u b = c u x u d