Fix a shadowed lemma name

[IlmariReissumies]

No description provided.

[mn200]

Thanks! (I have a follow up to prove elimination of Tau and make it an automatic rewrite.)

[mn200]

Follow up is cff397e

[IlmariReissumies]

There's already the following, which is equivalent to your itree_wbisim_tau_eqn0:

  !t t'. itree_wbisim (Tau t) t' ==> itree_wbisim t t'
Proof
  ho_match_mp_tac itree_wbisim_strong_coind \\ rw[] \\
  qhdtm_x_assum ‘itree_wbisim’
                (strip_assume_tac o ONCE_REWRITE_RULE[itree_wbisim_cases]) \\
  gvs[] \\
  metis_tac[itree_wbisim_cases]
QED```

...that said, automated rewrites seem reasonable to me.

[mn200]

That is the theorem in the other direction: I need it and my new result to get the iff.