# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265204359 -3600
# Node ID 34220518cccf24b0a424fbba4c23d81423f137ca
# Parent  68bdd55236083330c485e211ac71892c2952e1af
Simplified the proof.

diff -r 68bdd5523608 -r 34220518cccf Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 14:36:48 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 14:39:19 2010 +0100
@@ -823,9 +823,8 @@
 sorry
 
 lemma bv_list_rsp:
-  shows "t \<approx>5 s \<Longrightarrow> True"
-  and "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
-apply(induct rule: alpha5_alphalts.inducts)
+  shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
+apply(induct rule: alpha5_alphalts.inducts(2))
 apply(simp_all)
 done