--- a/Quot/Examples/LamEx.thy	Thu Jan 14 17:57:20 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 18:35:38 2010 +0100
@@ -256,11 +256,15 @@
 apply(default)
 sorry
 
+lemma fresh_lam:
+  "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)"
+sorry
+
 lemma lam_induct_strong:
   fixes a::"'a::fs_name"
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
-  and     a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
+  and     a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
   shows "P a lam"
 proof -
   have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" 
@@ -281,12 +285,27 @@
       apply (rule b2)
       done
   next
-    case (3 name lam pi)
-    have b: "P a (pi \<bullet> lam)" by fact
+    case (3 name lam pi a)
+    have b: "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" by fact
+    obtain c::name where fr: "c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)" sorry
+    from b fr have p: "P a (Lam c (([(c, pi\<bullet>name)]@pi)\<bullet>lam))" 
+      apply -
+      apply(rule a3)
+      apply(blast)
+      apply(simp)
+      done
+    have eq: "[(c, pi\<bullet>name)] \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)"
+      apply(rule perm_fresh_fresh)
+      using fr
+      apply(simp add: fresh_lam)
+      apply(simp add: fresh_lam)
+      done
     show "P a (pi \<bullet> Lam name lam)" 
       apply (simp add: pi_lam)
-      using b
-      sorry
+      apply(subst eq[symmetric])
+      using p
+      apply(simp only: pi_lam pt_name2 swap_simps)
+      done
   qed
   then have "P a (([]::name prm) \<bullet> lam)" by blast
   then show "P a lam" by simp