--- a/TODO	Thu Apr 08 10:25:38 2010 +0200
+++ b/TODO	Thu Apr 08 11:40:13 2010 +0200
@@ -35,6 +35,13 @@
   (both are equivalent, but the second seems to be closer to
    the fv-function)
 
+- when there are more than one shallow binder, then alpha
+  equivalence creates more than one permutation. According
+  to the paper, this is incorrect.
+
+  Example in TestMorePerm.
+
+
 - nested recursion, like types "trm list" in a constructor
 
 - define permute_bn automatically and prove properties of it