proposition: Lemma eutt_inv_vis {U : Type} (e : E U) (k1 k2 : U -> itree E R) : Vis e k1 ≈ Vis e k2 -> (forall u, k1 u ≈ k2 u).
proof: Proof. apply ITree.Eq.Eqit.eqit_inv_Vis; auto. Qed.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion ITree(Eq.Eqit Eq.UpToTaus Interp.InterpFacts Interp.RecursionFacts)