# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270076705 -7200
# Node ID be28f7b4b97b5106d972e3f003f3c610b8a1924d
# Parent  8b6a285ad480a1a88b1fe4f083d65d10a6105d00
added an item about alpha-equivalence (the existential should be closer to the abstraction)

diff -r 8b6a285ad480 -r be28f7b4b97b TODO
--- 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