[STATEMENT]
lemma lookup_eqvt[eqvt]:
  fixes pi::"name prm"
  and   \<theta>::"(name\<times>trm) list"
  and   x::"name"
  shows "pi \<bullet> (lookup \<theta> x) = lookup (pi \<bullet> \<theta>) (pi \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> lookup \<theta> x = lookup (pi \<bullet> \<theta>) (pi \<bullet> x)
[PROOF STEP]
by (induct \<theta>) (auto simp add: eqvts)