equal
deleted
inserted
replaced
24 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
24 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
25 apply (simp add: fresh_at_base Abs1_eq_iff) |
25 apply (simp add: fresh_at_base Abs1_eq_iff) |
26 apply (case_tac b) |
26 apply (case_tac b) |
27 apply (rule_tac y="a" in lt.strong_exhaust) |
27 apply (rule_tac y="a" in lt.strong_exhaust) |
28 apply auto[3] |
28 apply auto[3] |
29 apply blast |
29 apply blast+ |
30 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
30 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
31 apply (simp add: fresh_at_base Abs1_eq_iff) |
31 apply (simp add: fresh_at_base Abs1_eq_iff) |
32 apply blast |
|
33 --"-" |
32 --"-" |
34 apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))") |
33 apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))") |
35 apply (simp only:) |
34 apply (simp only:) |
36 apply (simp add: Abs1_eq_iff) |
35 apply (simp add: Abs1_eq_iff) |
37 apply (case_tac "c=ca") |
36 apply (case_tac "c=ca") |