439 lemma trans_eqvt[eqvt]:

   440   "p \<bullet> trans t l n = trans (p \<bullet>t) (p \<bullet>l) (p \<bullet>n)"

   441 proof (nominal_induct t avoiding: l p arbitrary: n rule: lam.strong_induct)

   442   fix name l n p

   443   show "p \<bullet> trans (Var name) l n =

   444        trans (p \<bullet> Var name) (p \<bullet> l) (p \<bullet> n)"

   445     apply (induct l arbitrary: n)

   446     apply simp

   447     apply auto

   448     apply (simp add: permute_pure)

   449     done

   450 next

   451   fix lam1 lam2 l n p

   452   assume 

   453     "\<And>b ba n. ba \<bullet> trans lam1 b n = trans (ba \<bullet> lam1) (ba \<bullet> b) (ba \<bullet> n)"

   454   "  \<And>b ba n. ba \<bullet> trans lam2 b n = trans (ba \<bullet> lam2) (ba \<bullet> b) (ba \<bullet> n)"

   455   then show "p \<bullet> trans (App lam1 lam2) l n =

   456           trans (p \<bullet> App lam1 lam2) (p \<bullet> l) (p \<bullet> n)"

   457     by (simp add: db_in_eqvt)

   458 next

   459   fix name :: name and l :: "name list" and p :: perm

   460   fix lam n

   461   assume

   462     "atom name \<sharp> l"

   463     "atom name \<sharp> p"

   464     "\<And>b ba n. ba \<bullet> trans lam b n = trans (ba \<bullet> lam) (ba \<bullet> b) (ba \<bullet> n)"

   465   then show

   466     "p \<bullet> trans (Lam [name]. lam) l n =

   467           trans (p \<bullet> Lam [name]. lam) (p \<bullet> l) (p \<bullet> n)"

   468   apply (simp add: fresh_at_list)

   469   apply (subst trans.simps)

   470   apply (simp add: fresh_at_list[symmetric])

   471   apply (simp add: db_in_eqvt)

   472   done

   473 qed

   474