diff -r 6ad2f1c296a7 -r aaaed6367b8f Nominal/Ex/LetRecB.thy
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:49:48 2011 +0100
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:01:15 2011 +0900
@@ -143,9 +143,25 @@
   apply(perm_simp)
   apply(simp)
   apply(simp add: inj_on_def)
-  --"HERE"
-  thm Abs_lst_fcb Abs_lst_fcb2
-  apply (drule_tac c="()" and ba="bn" in Abs_lst_fcb2)
+  --"The following could be done by nominal"
+  apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
+  apply (simp add: meta_eq_to_obj_eq[OF height_bp_def, symmetric, unfolded fun_eq_iff])
+  apply (subgoal_tac "eqvt_at height_bp bp")
+  apply (subgoal_tac "eqvt_at height_bp bpa")
+  apply (subgoal_tac "eqvt_at height_trm b")
+  apply (subgoal_tac "eqvt_at height_trm ba")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bp)")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bpa)")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl b)")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl ba)")
+  defer
+  apply (simp add: eqvt_at_def height_trm_def)
+  apply (simp add: eqvt_at_def height_trm_def)
+  apply (simp add: eqvt_at_def height_bp_def)
+  apply (simp add: eqvt_at_def height_bp_def)
+  --"I'd like to apply FCB here, but the following fails"
+  apply (erule_tac c="()" and ba="bn" in Abs_lst_fcb2)
+
   prefer 8
   apply(assumption)
   apply (drule_tac c="()" in Abs_lst_fcb2)