--- a/Quot/Examples/LamEx.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -71,6 +71,9 @@
 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
        \<Longrightarrow> rLam a t \<approx> rLam b s"
 
+
+
+
 (* should be automatic with new version of eqvt-machinery *)
 lemma alpha_eqvt:
   fixes pi::"name prm"
@@ -573,6 +576,17 @@
 lemma term1_hom_rsp:
   "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk>
        \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)"
+apply(simp)
+apply(rule allI)+
+apply(rule impI)
+apply(erule alpha.induct)
+apply(auto)[1]
+apply(auto)[1]
+apply(simp)
+apply(erule conjE)+
+apply(erule exE)+
+apply(erule conjE)+
+apply(clarify)
 sorry
 
 lemma hom: "