--- a/Paper/Paper.thy	Wed Mar 31 16:27:44 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 16:27:57 2010 +0200
@@ -1489,10 +1489,13 @@
   obtain by simple calculations the equalities.
   \end{proof}
 
-  With the above equations we can substitute free variables for support in
-  the lifted free variable equations, which gives us the support equations
-  for the term constructors. With this we can show that for each binding in
-  a constructors the bindings can be renamed. 
+%%% Without defining permute_bn, we cannot even write the substitution
+%%% of bindings in term constructors...
+
+% With the above equations we can substitute free variables for support in
+% the lifted free variable equations, which gives us the support equations
+% for the term constructors. With this we can show that for each binding in
+% a constructors the bindings can be renamed.
 
 *}