--- a/Nominal/Ex/SingleLet.thy	Mon Aug 16 17:59:09 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Mon Aug 16 19:57:41 2010 +0800
@@ -33,6 +33,7 @@
 (* cannot lift yet *)
 thm eq_iff
 thm eq_iff_simps
+(* bn / eqvt lemmas for fv / fv_bn / bn *)
 
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
@@ -63,39 +64,16 @@
 
 lemma [quot_respect]:
   "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
-  "(op = ===> (alpha_trm_raw ===> op =) ===> prod_rel op = alpha_trm_raw ===> op =) prod_fv prod_fv"
-  "((prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =) ===>
-         (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
-            prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===>
-            prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =)
-            prod_alpha prod_alpha" 
-  "(op = ===>
-         (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
-            prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =)
-            prod_alpha prod_alpha"
-  "((prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===>
-             prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =) ===>
-            (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===>
-            prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===>
-            prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===>
-            op =)
-            prod_alpha prod_alpha"
 sorry
 
-thm eq_iff(5)
-thm eq_iff(5)[unfolded alphas permute_prod.simps]
+
 ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
-   @{thms eq_iff(5)[unfolded alphas permute_prod.simps]}
+ val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
+   @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases]}
 *}
 
-ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]}
-*}
 
-ML {*
-  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas]}
-*}