[STATEMENT]
lemma psubst_ty_eqvt[eqvt]:
  fixes pi::"tvar prm"
  and   \<theta>::"Subst"
  and   T::"ty"
  shows "pi\<bullet>(\<theta><T>) = (pi\<bullet>\<theta>)<(pi\<bullet>T)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> \<theta><T> = (pi \<bullet> \<theta>)<pi \<bullet> T>
[PROOF STEP]
by (induct T rule: ty.induct) (simp_all add: eqvts)