--- a/Nominal/Term5.thy	Wed Mar 10 15:40:15 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 10 16:58:14 2010 +0100
@@ -90,15 +90,15 @@
 print_theorems
 
 lemma alpha5_rfv:
-  "(t \<approx>5 s \<longrightarrow> fv_rtrm5 t = fv_rtrm5 s) \<and> (l \<approx>l m \<longrightarrow> fv_rlts l = fv_rlts m) \<and> (alpha_rbv5 a b c \<longrightarrow> True)"
-  apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+  "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
+  "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m))"
+  "(alpha_rbv5 a b c \<Longrightarrow> True)"
+  apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
   apply(simp_all)
   apply(simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(erule exE)
-  apply(erule conjE)+
+  apply(clarify)
   apply(simp_all)
-  sorry
+  sorry (* works for non-rec *)
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
@@ -122,18 +122,20 @@
   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
   apply (clarify)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-  defer
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha5_inj)
+  apply clarify
   apply clarify
-  apply (erule alpha_rlts.cases)
-  apply (erule alpha_rlts.cases)
-  apply (simp_all)
-  defer
-  apply (erule alpha_rlts.cases)
-  apply (simp_all)
-  defer
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply simp_all
+  apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply simp_all
+  defer defer (* Both sides false, so equal when we have distinct *)
+  apply (erule conjE)+
   apply clarify
   apply (simp add: alpha5_inj)
   sorry (* may be true? *)
+
 lemma
   shows "(alpha_rlts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)