proposition: Lemma eqitree_inv_Vis_r {E R U} (t : itree E R) (e : E U) (k : U -> _) : t ≅ Vis e k -> exists k', observe t = VisF e k' /\ forall u, k' u ≅ k u.
proof: Proof. intros; punfold H; apply eqitF_inv_VisF_r in H. destruct H as [ [? [-> ?]] | [] ]; [ | discriminate ]. pclearbot. eexists; split; eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)