121   "finite (set (bn l))"

   121   "finite (set (bn l))"

   122   apply(induct l rule: trm_lts.inducts(2))

   122   apply(induct l rule: trm_lts.inducts(2))

   123   apply(simp_all add:permute_bn eqvts)

   123   apply(simp_all add:permute_bn eqvts)

   124   done

   124   done

   125 

   125 

   126 lemma 

   128 lemma 

   127   fixes t::trm

   129   fixes t::trm

   128   and   l::lts

   130   and   l::lts

   129   and   c::"'a::fs"

   131   and   c::"'a::fs"

   130   assumes a1: "\<And>name c. P1 c (Vr name)"

   132   assumes a1: "\<And>name c. P1 c (Vr name)"