Prove (or disprove) "iter after iter" equation

[Lysxia]

@YaZko wondered about this equation to rewrite the sequential composition of two iter:

iter f >>> iter g
=
inl_ >>> iter (case_ (f >>> inl_) (g >>> inr_ >>> assoc_l))

Because the equation looks similar to theorems we've already proved about loop rather than iter, I think it's provable from the iterative axioms but haven't succeeded at it. Another way is to specialize it to itree and construct the bisimulation explicitly.

It might actually be simpler and more interesting to implement a solver to settle this type of question once and for all, although I don't know whether the problem is decidable.

[YaZko]

I proved the equation in the special case of itrees (see db77cb9).

I remain very curious as to whether it can be proved abstractly.
Certainly investigating the decidability of all the equational theory sounds interesting!