--- a/Quot/Examples/LamEx.thy	Fri Jan 15 12:17:30 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 15:51:25 2010 +0100
@@ -360,26 +360,49 @@
   apply(simp add: var_supp1)
   done
 
+(* lemma hom_reg: *)
 
 lemma hom: "
-\<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
-\<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
-  \<exists>hom \<in> Respects(alpha ===> op =). (
+  \<exists>hom\<in>Respects (alpha ===> op =). (
     (\<forall>x. hom (rVar x) = f_var x) \<and>
     (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
     (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
   )"
 sorry
 
+lemma hom_reg:"
+(\<exists>hom\<in>Respects (alpha ===> op =).
+ (\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa)))) \<longrightarrow>
+(\<exists>hom.
+ (\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))"
+by(regularize)
+
+thm impE[OF hom_reg]
+lemma hom_pre:"
+(\<exists>hom.
+ (\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))"
+apply (rule impE[OF hom_reg])
+apply (rule hom)
+apply (assumption)
+done
+
 lemma hom':
-"\<forall>f_lam. \<forall>f_app. \<exists>hom. (
+"\<exists>hom. (
     (\<forall>x. hom (Var x) = f_var x) \<and>
     (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and>
     (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
   )"
-(*apply (lifting hom)*)
-sorry
+apply (lifting hom)
+done
 
-thm rlam.recs
+thm bex_reg_eqv_range[OF identity_equivp, of "alpha"]
+
 
 end
+