equal
deleted
inserted
replaced
1705 by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod) |
1705 by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod) |
1706 next |
1706 next |
1707 case (AndR c1 M c2 M' c3) |
1707 case (AndR c1 M c2 M' c3) |
1708 then show ?case |
1708 then show ?case |
1709 apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left) |
1709 apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left) |
1710 apply (metis (erased, hide_lams)) |
1710 apply (metis (erased, opaque_lifting)) |
1711 by metis |
1711 by metis |
1712 next |
1712 next |
1713 case AndL1 |
1713 case AndL1 |
1714 then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod) |
1714 then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod) |
1715 next |
1715 next |