165     apply(simp add: trm_lts.fv[simplified trm_lts.supp])

   165     apply(simp add: trm_lts.fv[simplified trm_lts.supp])

   166     apply(simp)

   166     apply(simp)

   167     apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")

   167     apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")

   168     apply(erule exE)

   168     apply(erule exE)

   169     apply(erule conjE)

   169     apply(erule conjE)

   170     apply(subst Lt_subst)

   171     apply(subst Lt_subst)

   171     apply assumption

   172     apply assumption

   172     apply(rule a4)

   173     apply(rule a4)

   173     apply(simp add:perm_bn[symmetric])

   174     apply(simp add:perm_bn[symmetric])

   174     apply(simp add: eqvts)

   175     apply(simp add: eqvts)