120   apply (case_tac x rule: trm_assn.exhaust(1))

   120   apply (case_tac x rule: trm_assn.exhaust(1))

   121   apply (auto)[4]

   121   apply (auto)[4]

   122   apply (drule_tac x="assn" in meta_spec)

   122   apply (drule_tac x="assn" in meta_spec)

   123   apply (drule_tac x="trm" in meta_spec)

   123   apply (drule_tac x="trm" in meta_spec)

   124   apply (simp add: alpha_bn_refl)

   124   apply (simp add: alpha_bn_refl)

   125   apply(simp_all)

   126   apply(simp_all)

   126   apply (erule_tac c="()" in Abs_lst1_fcb2)

   127   apply (erule_tac c="()" in Abs_lst1_fcb2)

   127   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)[4]

   128   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)[4]

   128   apply (erule conjE)

   129   apply (erule conjE)

   129   apply (subst alpha_bn_apply_assn)

   130   apply (subst alpha_bn_apply_assn)

   177   apply (drule_tac x="assn" in meta_spec)

   178   apply (drule_tac x="assn" in meta_spec)

   178   apply (simp add: Abs1_eq_iff alpha_bn_refl)

   179   apply (simp add: Abs1_eq_iff alpha_bn_refl)

   179   apply simp_all[7]

   180   apply simp_all[7]

   180   prefer 2

   181   prefer 2

   181   apply(simp)

   182   apply(simp)

   182   apply(simp)

   184   apply(simp)

   183   apply(erule conjE)+

   185   apply(erule conjE)+

   184   apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)

   186   apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)

   185   apply (simp add: Abs_fresh_iff)

   187   apply (simp add: Abs_fresh_iff)

   186   apply (simp add: fresh_star_def)

   188   apply (simp add: fresh_star_def)