--- a/Paper/Paper.thy	Wed Mar 31 17:04:09 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 17:51:15 2010 +0200
@@ -1454,7 +1454,7 @@
   \end{tabular}
   \end{center}
 
-  Notice that until now we have not said anything about the support of the
+  Until now we have not said anything about the support of the
   defined type. This is because we could not use the general definition of
   support in lifted theorems, since it does not preserve the relation.
   Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"},
@@ -1504,16 +1504,52 @@
   obtain by simple calculations the equalities.
   \end{proof}
 
-%%% 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. To rename a shallow binder
+  or a deep recursive binder a permutation is sufficient. This is not the
+  case for a deep non-recursive bindings. Take the term
+  @{text "Let (ACons x (Vr x) ANil) (Vr x)"}, representing the language construct
+  @{text "let x = x in x"}. To rename the binder the permutation cannot
+  be applied to the whole assignment since it would rename the free @{term "x"}
+  as well. To avoid this we introduce a new construction operation
+  that applies a permutation under a binding function.
 
-% 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.
+  For each binding function @{text "bn\<^isub>j :: ty\<^isub>i \<Rightarrow> \<dots>"} we define a permutation operation
+  @{text "\<bullet>bn\<^isub>j\<^isub> :: perm \<Rightarrow> ty\<^isub>i \<Rightarrow> ty\<^isub>i"}. This operation permutes only the arguments
+  that are bound by the binding function while also descending in the recursive subcalls.
+  For each term constructor @{text "C x\<^isub>1 \<dots> x\<^isub>n"} the @{text "\<bullet>bn\<^isub>j"} operation applied
+  to a permutation @{text "\<pi>"} and to this constructor equals the constructor applied
+  to the values for each argument. Provided @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, the value
+  for an argument @{text "x\<^isub>j"} is:
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  $\bullet$ & @{text "x\<^isub>i"} provided @{text "x\<^isub>i"} is not in @{text "rhs"}\\
+  $\bullet$ & @{text "\<pi> \<bullet> x\<^isub>i"} provided @{text "x\<^isub>i"} is in @{text "rhs"} without a binding function\\
+  $\bullet$ & @{text "\<pi> \<bullet>bn\<^isub>k x\<^isub>i"} provided @{text "bn\<^isub>k x\<^isub>i"} is @{text "rhs"}\\
+  \end{tabular}
+  \end{center}
+
+  The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it
+  and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this defnition is correct is:
+
+%% We could get this from ExLet/perm_bn lemma.
+  \begin{lemma} For every bn function  @{text "bn\<^isup>\<alpha>\<^isub>i"},
+  \begin{center}
+  @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i l = bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i l)"}
+  \end{center}
+  \end{lemma}
+  \begin{proof} By induction on the lifted type it follows from the definitions of
+    permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.
+  \end{proof}
+
+
 
 *}
 
+(* @{thm "ACons_subst[no_vars]"}*)
+
 text {*
 %%% FIXME: The restricions should have already been described in previous sections?
   Restrictions