equal
deleted
inserted
replaced
96 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
96 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
97 apply (simp add: Abs1_eq_iff) |
97 apply (simp add: Abs1_eq_iff) |
98 apply blast |
98 apply blast |
99 --"" |
99 --"" |
100 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
100 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
101 apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
101 apply (subgoal_tac "Lam b (Sum_Type.projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
102 apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
102 apply (subgoal_tac "Lam ba (Sum_Type.projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
103 apply (simp only:) |
103 apply (simp only:) |
104 apply (erule Abs_lst1_fcb) |
104 apply (erule Abs_lst1_fcb) |
105 apply (simp add: Abs_fresh_iff) |
105 apply (simp add: Abs_fresh_iff) |
106 apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2] |
106 apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2] |
107 (* need an invariant to get eqvt_at (Proj) *) |
107 (* need an invariant to get eqvt_at (Proj) *) |