[STATEMENT]
lemma eqvt_at_apply'':
  assumes "eqvt_at f x"
  shows "(p \<bullet> f) (p \<bullet> x) = f (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> f) (p \<bullet> x) = f (p \<bullet> x)
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))