# HG changeset patch
# User urbanc
# Date 1198109241 -3600
# Node ID 0a104ddb72d92a27614ea9ee43a42cca7786bfc7
# Parent  5ae1dc2bb5ea3fc1c00afb5cd27e09f3265b8af0
polishing of some proofs

diff -r 5ae1dc2bb5ea -r 0a104ddb72d9 src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Thu Dec 20 00:19:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Thu Dec 20 01:07:21 2007 +0100
@@ -1,4 +1,4 @@
-(* $Id: *)
+(* $Id$ *)
 
 theory Contexts
 imports "../Nominal"
@@ -19,20 +19,18 @@
 
 atom_decl name
 
-text {* terms *}
-
+text {* Terms *}
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-text {* contexts - the context-lambda does not bind anything *}
-
+text {* Contexts - the lambda case in contexts does not bind a name *}
 nominal_datatype ctx = 
     Hole
   | CAppL "ctx" "lam"
   | CAppR "lam" "ctx" 
-  | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100)
+  | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100) 
 
 text {* Capture-avoiding substitution and three lemmas *}
 
@@ -61,17 +59,10 @@
 by (nominal_induct t avoiding: x y t' rule: lam.inducts)
    (auto simp add: abs_fresh fresh_prod fresh_atm)
 
-lemma subst_swap: 
-  fixes x y::"name"
-  and   t t'::"lam"
-  shows   "y\<sharp>t \<Longrightarrow> ([(y,x)]\<bullet>t)[y::=t'] = t[x::=t']"
-by (nominal_induct t avoiding: x y t' rule: lam.inducts)
-   (auto simp add: lam.inject calc_atm fresh_atm abs_fresh)
-
 text {* 
-  The operation that fills one term into a hole. While
-  contexts are not alpha-equivalence classes, the filling
-  operation produces an alpha-equivalent lambda-term. 
+  Replace is the operation that fills a term into a hole. While
+  contexts themselves are not alpha-equivalence classes, the 
+  filling operation produces an alpha-equivalent lambda-term. 
 *}
 
 consts 
@@ -81,13 +72,15 @@
   "Hole<t> = t"
   "(CAppL E t')<t> = App (E<t>) t'"
   "(CAppR t' E)<t> = App t' (E<t>)"
-  "(CLam [x].E)<t> = Lam [x].(E<t>)"
+  "(CLam [x].E)<t> = Lam [x].(E<t>)" 
 by (rule TrueI)+
 
+
 lemma alpha_test: 
   shows "(CLam [x].Hole)<Var x> = (CLam [y].Hole)<Var y>"
 by (auto simp add: alpha lam.inject calc_atm fresh_atm) 
 
+
 lemma replace_eqvt[eqvt]:
   fixes pi:: "name prm"
   shows "pi\<bullet>(E<e>) = (pi\<bullet>E)<(pi\<bullet>e)>"
@@ -101,7 +94,8 @@
 by (induct E rule: ctx.weak_induct)
    (auto simp add: fresh_prod abs_fresh)
 
-text {* composition of two contexts *}
+
+text {* Composition of two contexts *}
 
 consts 
  ctx_replace :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
@@ -124,7 +118,7 @@
 by (induct E1 rule: ctx.weak_induct)
    (auto simp add: fresh_prod)
 
-text {* beta-reduction via contexts *}
+text {* Beta-reduction via contexts *}
 
 inductive
   ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) 
@@ -136,7 +130,7 @@
 nominal_inductive ctx_red
   by (simp_all add: replace_fresh subst_fresh abs_fresh)
 
-text {* beta-reduction via congruence rules *}
+text {* Beta-reduction via congruence rules *}
 
 inductive
   cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) 
@@ -151,7 +145,7 @@
 nominal_inductive cong_red
   by (simp_all add: subst_fresh abs_fresh)
 
-text {* the proof that shows both relations are equal *}
+text {* The proof that shows both relations are equal *}
 
 lemma cong_red_ctx:
   assumes a: "t \<longrightarrow>o t'"
diff -r 5ae1dc2bb5ea -r 0a104ddb72d9 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Thu Dec 20 00:19:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Thu Dec 20 01:07:21 2007 +0100
@@ -18,7 +18,8 @@
   "Crary",
   "SOS",
   "LocalWeakening",
-  "Support"
+  "Support",
+  "Contexts" 
 ];
 
-setmp quick_and_dirty true use_thy "VC_Compatible";
\ No newline at end of file
+setmp quick_and_dirty true use_thy "VC_Condition";
\ No newline at end of file
diff -r 5ae1dc2bb5ea -r 0a104ddb72d9 src/HOL/Nominal/Examples/VC_Compatible.thy
--- a/src/HOL/Nominal/Examples/VC_Compatible.thy	Thu Dec 20 00:19:40 2007 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,184 +0,0 @@
-(* $Id$ *)
-
-theory VC_Compatible
-imports "../Nominal" 
-begin
-
-text {* 
-  We give here two examples that show if we use the variable  
-  convention carelessly in rule inductions, we might end 
-  up with faulty lemmas. The point is that the examples
-  are not variable-convention compatible and therefore in the 
-  nominal package one is protected from such bogus reasoning.
-*}
-
-text {* 
-  We define alpha-equated lambda-terms as usual. *}
-atom_decl name 
-
-nominal_datatype lam = 
-    Var "name"
-  | App "lam" "lam"
-  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
-
-text {*
-  The inductive relation 'unbind' unbinds the top-most  
-  binders of a lambda-term; this relation is obviously  
-  not a function, since it does not respect alpha-      
-  equivalence. However as a relation 'unbind' is ok and     
-  a similar relation has been used in our formalisation 
-  of the algorithm W. *}
-inductive
-  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
-where
-  u_var: "(Var a) \<mapsto> [],(Var a)"
-| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
-| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
-
-text {*
-  We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x 
-  and also to [z,y],Var y (though the proof for the second is a 
-  bit clumsy). *} 
-lemma unbind_lambda_lambda1: 
-  shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
-by (auto intro: unbind.intros)
-
-lemma unbind_lambda_lambda2: 
-  shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
-proof -
-  have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" 
-    by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
-  moreover
-  have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
-    by (auto intro: unbind.intros)
-  ultimately 
-  show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
-qed
-
-text {* Unbind is equivariant ...*}
-equivariance unbind
-
-text {*
-  ... but it is not variable-convention compatible (see Urban, 
-  Berghofer, Norrish [2007] for more details). This condition 
-  requires for rule u_lam to have the binder x being not a free variable 
-  in the rule's conclusion. Because this condition is not satisfied, 
-  Isabelle will not derive a strong induction principle for 'unbind' 
-  - that means Isabelle does not allow us to use the variable 
-  convention in induction proofs over 'unbind'. We can, however,  
-  force Isabelle to derive the strengthening induction principle
-  and see what happens. *}
-
-nominal_inductive unbind
-  sorry
-
-text {*
-  To obtain a faulty lemma, we introduce the function 'bind'
-  which takes a list of names and abstracts away these names in 
-  a given lambda-term. *}
-fun 
-  bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
-where
-  "bind [] t = t"
-| "bind (x#xs) t = Lam [x].(bind xs t)"
-
-text {*
-  Although not necessary for our main argument below, we can 
-  easily prove that bind undoes the unbinding. *}
-lemma bind_unbind:
-  assumes a: "t \<mapsto> xs,t'"
-  shows "t = bind xs t'"
-using a by (induct) (auto)
-
-text {*
-  The next lemma shows by induction on xs that if x is a free 
-  variable in t and x does not occur in xs, then x is a free 
-  variable in bind xs t. In the nominal tradition we formulate    
-  'is a free variable in' as 'is not fresh for'. *}
-lemma free_variable:
-  fixes x::"name"
-  assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
-  shows "\<not>(x\<sharp>bind xs t)"
-using a b
-by (induct xs)
-   (auto simp add: fresh_list_cons abs_fresh fresh_atm)
-
-text {*
-  Now comes the faulty lemma. It is derived using the     
-  variable convention (i.e. our strong induction principle). 
-  This faulty lemma states that if t unbinds to x::xs and t', 
-  and x is a free variable in t', then it is also a free 
-  variable in bind xs t'. We show this lemma by assuming that 
-  the binder x is fresh w.r.t. to the xs unbound previously. *}   
-
-lemma faulty1:
-  assumes a: "t\<mapsto>(x#xs),t'"
-  shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
-using a
-by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
-   (simp_all add: free_variable)
-
-text {*
-  Obviously the faulty lemma does not hold, for example, in 
-  case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). Therefore,
-  we can prove False. *}
-
-lemma false1:
-  shows "False"
-proof -
-  have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" 
-  and  "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
-  then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
-  moreover 
-  have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh)
-  ultimately
-  show "False" by simp
-qed
-   
-text {* 
-  The next example is slightly simpler, but looks more
-  contrived than 'unbind'. This example, caled 'strip' just 
-  strips off the top-most binders from lambdas. *}
-
-inductive
-  strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
-where
-  s_var: "(Var a) \<rightarrow> (Var a)"
-| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
-| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
-
-text {* 
-  The relation is equivariant but we have to use again 
-  sorry to derive a strong induction principle. *}
-
-equivariance strip
-
-nominal_inductive strip
-  sorry
-
-text {*
-  The faulty lemma shows that a variable that is fresh
-  for a term is also fresh for the term after striping. *}
-
-lemma faulty2:
-  fixes x::"name"
-  assumes a: "t \<rightarrow> t'"
-  shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'"
-using a
-by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
-   (auto simp add: abs_fresh)
-
-text {*
-  Obviously Lam [x].Var x is a counter example to this lemma. *}
-
-lemma false2:
-  shows "False"
-proof -
-  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
-  moreover
-  have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh)
-  ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
-  then show "False" by (simp add: fresh_atm)
-qed 
- 
-end
\ No newline at end of file
diff -r 5ae1dc2bb5ea -r 0a104ddb72d9 src/HOL/Nominal/Examples/VC_Condition.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Thu Dec 20 01:07:21 2007 +0100
@@ -0,0 +1,184 @@
+(* $Id$ *)
+
+theory VC_Compatible
+imports "../Nominal" 
+begin
+
+text {* 
+  We give here two examples that show if we use the variable  
+  convention carelessly in rule inductions, we might end 
+  up with faulty lemmas. The point is that the examples
+  are not variable-convention compatible and therefore in the 
+  nominal package one is protected from such bogus reasoning.
+*}
+
+text {* 
+  We define alpha-equated lambda-terms as usual. *}
+atom_decl name 
+
+nominal_datatype lam = 
+    Var "name"
+  | App "lam" "lam"
+  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+
+text {*
+  The inductive relation 'unbind' unbinds the top-most  
+  binders of a lambda-term; this relation is obviously  
+  not a function, since it does not respect alpha-      
+  equivalence. However as a relation 'unbind' is ok and     
+  a similar relation has been used in our formalisation 
+  of the algorithm W. *}
+inductive
+  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
+where
+  u_var: "(Var a) \<mapsto> [],(Var a)"
+| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
+| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
+
+text {*
+  We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x 
+  and also to [z,y],Var y (though the proof for the second is a 
+  bit clumsy). *} 
+lemma unbind_lambda_lambda1: 
+  shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
+by (auto intro: unbind.intros)
+
+lemma unbind_lambda_lambda2: 
+  shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
+proof -
+  have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" 
+    by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
+  moreover
+  have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
+    by (auto intro: unbind.intros)
+  ultimately 
+  show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
+qed
+
+text {* Unbind is equivariant ...*}
+equivariance unbind
+
+text {*
+  ... but it is not variable-convention compatible (see Urban, 
+  Berghofer, Norrish [2007] for more details). This condition 
+  requires for rule u_lam to have the binder x being not a free variable 
+  in the rule's conclusion. Because this condition is not satisfied, 
+  Isabelle will not derive a strong induction principle for 'unbind' 
+  - that means Isabelle does not allow us to use the variable 
+  convention in induction proofs over 'unbind'. We can, however,  
+  force Isabelle to derive the strengthening induction principle
+  and see what happens. *}
+
+nominal_inductive unbind
+  sorry
+
+text {*
+  To obtain a faulty lemma, we introduce the function 'bind'
+  which takes a list of names and abstracts away these names in 
+  a given lambda-term. *}
+fun 
+  bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "bind [] t = t"
+| "bind (x#xs) t = Lam [x].(bind xs t)"
+
+text {*
+  Although not necessary for our main argument below, we can 
+  easily prove that bind undoes the unbinding. *}
+lemma bind_unbind:
+  assumes a: "t \<mapsto> xs,t'"
+  shows "t = bind xs t'"
+using a by (induct) (auto)
+
+text {*
+  The next lemma shows by induction on xs that if x is a free 
+  variable in t and x does not occur in xs, then x is a free 
+  variable in bind xs t. In the nominal tradition we formulate    
+  'is a free variable in' as 'is not fresh for'. *}
+lemma free_variable:
+  fixes x::"name"
+  assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
+  shows "\<not>(x\<sharp>bind xs t)"
+using a b
+by (induct xs)
+   (auto simp add: fresh_list_cons abs_fresh fresh_atm)
+
+text {*
+  Now comes the faulty lemma. It is derived using the     
+  variable convention (i.e. our strong induction principle). 
+  This faulty lemma states that if t unbinds to x::xs and t', 
+  and x is a free variable in t', then it is also a free 
+  variable in bind xs t'. We show this lemma by assuming that 
+  the binder x is fresh w.r.t. to the xs unbound previously. *}   
+
+lemma faulty1:
+  assumes a: "t\<mapsto>(x#xs),t'"
+  shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
+using a
+by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
+   (simp_all add: free_variable)
+
+text {*
+  Obviously the faulty lemma does not hold, for example, in 
+  case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). Therefore,
+  we can prove False. *}
+
+lemma false1:
+  shows "False"
+proof -
+  have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" 
+  and  "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
+  then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
+  moreover 
+  have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh)
+  ultimately
+  show "False" by simp
+qed
+   
+text {* 
+  The next example is slightly simpler, but looks more
+  contrived than 'unbind'. This example, caled 'strip' just 
+  strips off the top-most binders from lambdas. *}
+
+inductive
+  strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
+where
+  s_var: "(Var a) \<rightarrow> (Var a)"
+| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
+| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
+
+text {* 
+  The relation is equivariant but we have to use again 
+  sorry to derive a strong induction principle. *}
+
+equivariance strip
+
+nominal_inductive strip
+  sorry
+
+text {*
+  The faulty lemma shows that a variable that is fresh
+  for a term is also fresh for the term after striping. *}
+
+lemma faulty2:
+  fixes x::"name"
+  assumes a: "t \<rightarrow> t'"
+  shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'"
+using a
+by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
+   (auto simp add: abs_fresh)
+
+text {*
+  Obviously Lam [x].Var x is a counter example to this lemma. *}
+
+lemma false2:
+  shows "False"
+proof -
+  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
+  moreover
+  have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh)
+  ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
+  then show "False" by (simp add: fresh_atm)
+qed 
+ 
+end
\ No newline at end of file
diff -r 5ae1dc2bb5ea -r 0a104ddb72d9 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Thu Dec 20 00:19:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Thu Dec 20 01:07:21 2007 +0100
@@ -1,11 +1,10 @@
 (* $Id$ *)
 
 theory Weakening 
-imports "../Nominal" 
+  imports "../Nominal" 
 begin
 
 section {* Weakening Example for the Simply-Typed Lambda-Calculus *}
-(*================================================================*)
 
 atom_decl name 
 
@@ -28,7 +27,8 @@
 
 text {* 
   Valid contexts (at the moment we have no type for finite 
-  sets yet; therefore typing-contexts are lists). *}
+  sets yet; therefore typing-contexts are lists). 
+  *}
 inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
@@ -46,9 +46,10 @@
   | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
 
 text {* 
-  We automatically derive the strong induction principle 
-  for the typing relation (this induction principle has the 
-  variable convention already built in). *}
+  We derive the strong induction principle for the typing 
+  relation (this induction principle has the variable convention 
+  already built in). 
+  *}
 equivariance typing
 nominal_inductive typing
   by (simp_all add: abs_fresh ty_fresh)
@@ -60,11 +61,11 @@
   "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
 
 text {* Now it comes: The Weakening Lemma *}
-(*========================================*)
 
 text {* 
   The first version is, after setting up the induction, 
-  quite automatic except for use of atomize. *}
+  completely automatic except for use of atomize. 
+  *}
 lemma weakening_version1: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T" 
@@ -77,7 +78,8 @@
 
 text {* 
   The second version gives all details for the variable
-  and lambda case. *}
+  and lambda case. 
+  *}
 lemma weakening_version2: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   and   t ::"lam"
@@ -111,7 +113,8 @@
 text{* 
   The original induction principle for the typing relation
   is not strong enough - even this simple lemma fails to be 
-  simple ;o) *}
+  simple ;o) 
+  *}
 lemma weakening_not_straigh_forward: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -140,8 +143,7 @@
   have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 
     oops
   
-text{* 
-  The complete proof without using the variable convention. *}
+text{* The complete proof without using the variable convention. *}
 lemma weakening_with_explicit_renaming: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -189,6 +191,7 @@
 text {*
   Compare the proof with explicit renamings to version1 and version2,
   and imagine you are proving something more substantial than the
-  weakening lemma. *}
+  weakening lemma. 
+  *}
 
 end
\ No newline at end of file