--- a/Nominal/Ex/CoreHaskell.thy	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 06:39:27 2010 +0800
@@ -88,6 +88,7 @@
 (* can lift *)
 thm distinct
 thm fv_defs
+thm alpha_bn_imps alpha_equivp
 
 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts
 thm perm_simps
@@ -128,7 +129,11 @@
   val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}
 *}
 
-
+ML {*
+ val thms_e = map (lift_thm qtys @{context}) 
+   @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases]}
+*}
 
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)