[STATEMENT]
lemma eqvtChainEq:
  fixes P    :: pi
  and   P'   :: pi
  and   perm :: "name prm"

  shows   "P \<Longrightarrow>\<^sub>\<tau> P' = (perm \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (perm \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P' = perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'
[PROOF STEP]
by(blast intro: eqvtChainE eqvtChainI)