--- a/TODO	Wed Mar 31 22:48:35 2010 +0200
+++ b/TODO	Thu Apr 01 01:05:05 2010 +0200
@@ -20,6 +20,21 @@
 
 Bigger things:
 
+- the alpha equivalence for
+
+   Let as::assn t::trm   bind "bn as" in t
+
+  creates as premise
+
+    EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t')
+
+  but I think it should be
+
+    as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t')    
+
+  (both are equivalent, but the second seems to be closer to
+   the fv-function)
+
 - nested recursion, like types "trm list" in a constructor
 
 - define permute_bn automatically and prove properties of it