349   shows "permute_trm4_list p ts = p \<bullet> ts"

   349   shows "permute_trm4_list p ts = p \<bullet> ts"

   350   apply(induct ts)

   350   apply(induct ts)

   351   apply(simp_all)

   351   apply(simp_all)

   352   done

   352   done

   353 

   353 

   354 thm permute_trm4_permute_trm4_list.simps[simplified repaired]

   355 thm permute_trm4_permute_trm4_list.simps[simplified repaired]

   355 

   356 

   356 inductive

   357 inductive

   357     alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)

   358     alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)

   358 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 

   359 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100)