--- a/Paper/Paper.thy	Wed Mar 31 12:30:17 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 15:20:58 2010 +0200
@@ -1479,10 +1479,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.
 
 *}