equal
deleted
inserted
replaced
55 and b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
55 and b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
56 and c1: "(t,r)\<in>it f1 f2 f3" |
56 and c1: "(t,r)\<in>it f1 f2 f3" |
57 and c2: "(t,r')\<in>it f1 f2 f3" |
57 and c2: "(t,r')\<in>it f1 f2 f3" |
58 shows "r=r'" |
58 shows "r=r'" |
59 using c1 c2 |
59 using c1 c2 |
60 proof (induct fixing: r') |
60 proof (induct arbitrary: r') |
61 case it1 |
61 case it1 |
62 then show ?case by cases (simp_all add: lam.inject) |
62 then show ?case by cases (simp_all add: lam.inject) |
63 next |
63 next |
64 case (it2 r1 r2 t1 t2) |
64 case (it2 r1 r2 t1 t2) |
65 have ih1: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact |
65 have ih1: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact |