diff -r ec0afa89aab3 -r 4abb95a7264b Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 10:57:49 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 11:34:43 2010 +0200
@@ -562,7 +562,7 @@
   @{thm[mode=IfThen] supp_perm_eq[no_vars]}
   \end{property}
 
-  \begin{property}
+  \begin{property}\label{avoiding}
   For a finite set @{text as} and a finitely supported @{text x} with
   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
   exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
@@ -1630,8 +1630,8 @@
 %% We could get this from ExLet/perm_bn lemma.
   \begin{lemma} For every bn function  @{text "bn\<^isup>\<alpha>\<^isub>i"},
   \begin{eqnarray}
-  @{term "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\
-  @{term "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}
+  @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\
+  @{text "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}
   \end{eqnarray}
   \end{lemma}
   \begin{proof} By induction on the lifted type it follows from the definitions of
@@ -1641,6 +1641,26 @@
 
 *}
 
+section {* Strong Induction Principles *}
+
+text {*
+  With the help of @{text "\<bullet>bn"} functions defined in the previous section
+  we can show that binders can be substituted in term constructors. We show
+  this only for the specification from Figure~\ref{nominalcorehas}. The only
+  constructor with a complicated binding structure is @{text "ACons"}. For this
+  constructor we prove:
+  \begin{eqnarray}
+  \lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\
+  & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber
+  \end{eqnarray}
+
+  With the Property~\ref{avoiding} we can prove a strong induction principle
+  which we show again only for the Core Haskell example:
+
+  
+
+*}
+
 text {*
 
   \begin{figure}[t!]
@@ -1715,11 +1735,6 @@
   \end{figure}
 *}
 
-
-(* @{thm "ACons_subst[no_vars]"}*)
-
-section {* Strong Induction Principles *}
-
 section {* Related Work *}
 
 text {*