An issue with definition of eutt

[yjsongamz]

In the definition of eutt, it seems like vis, tau, taul, and taur cases all make coinductive progress.
If that is the case, the definition is flawed - it will equate infinite loop (spin) with anything.
The right definition is that only vis and tau case should make progress, but not for taul and taur.

[Kiiyya]

Oh! Thank you for spotting this! The correct definition should then be the following. If I have a spare moment in the coming days I'll fix this and any resulting definitions, but feel free to make a PR :)

inductive EuttF (R : ITree E A → ITree E A → Prop) : ITree E A → ITree E A → Prop
| ret : EuttF R (.ret r) (.ret r)
| vis : (∀ a, R (k₁ a) (k₂ a)) → EuttF R (.vis e k₁) (.vis e k₂)
| tau  : R x y → EuttF R (.tau x) (.tau y)
| taul : EuttF R x y → EuttF R (.tau x) y -- EuttF instead of just R
| taur : EuttF R x y → EuttF R x (.tau y)