141 apply (simp add: eqvt_at_def) |
141 apply (simp add: eqvt_at_def) |
142 apply(simp add: eqvt_def) |
142 apply(simp add: eqvt_def) |
143 apply(perm_simp) |
143 apply(perm_simp) |
144 apply(simp) |
144 apply(simp) |
145 apply(simp add: inj_on_def) |
145 apply(simp add: inj_on_def) |
146 --"HERE" |
146 --"The following could be done by nominal" |
147 thm Abs_lst_fcb Abs_lst_fcb2 |
147 apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff]) |
148 apply (drule_tac c="()" and ba="bn" in Abs_lst_fcb2) |
148 apply (simp add: meta_eq_to_obj_eq[OF height_bp_def, symmetric, unfolded fun_eq_iff]) |
|
149 apply (subgoal_tac "eqvt_at height_bp bp") |
|
150 apply (subgoal_tac "eqvt_at height_bp bpa") |
|
151 apply (subgoal_tac "eqvt_at height_trm b") |
|
152 apply (subgoal_tac "eqvt_at height_trm ba") |
|
153 apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bp)") |
|
154 apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bpa)") |
|
155 apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl b)") |
|
156 apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl ba)") |
|
157 defer |
|
158 apply (simp add: eqvt_at_def height_trm_def) |
|
159 apply (simp add: eqvt_at_def height_trm_def) |
|
160 apply (simp add: eqvt_at_def height_bp_def) |
|
161 apply (simp add: eqvt_at_def height_bp_def) |
|
162 --"I'd like to apply FCB here, but the following fails" |
|
163 apply (erule_tac c="()" and ba="bn" in Abs_lst_fcb2) |
|
164 |
149 prefer 8 |
165 prefer 8 |
150 apply(assumption) |
166 apply(assumption) |
151 apply (drule_tac c="()" in Abs_lst_fcb2) |
167 apply (drule_tac c="()" in Abs_lst_fcb2) |
152 apply (simp add: Abs_eq_iff2) |
168 apply (simp add: Abs_eq_iff2) |
153 apply (simp add: alphas) |
169 apply (simp add: alphas) |