proposition: Lemma eqit_inv_Vis {E R1 R2} (RR : R1 -> R2 -> Prop) b1 b2 U (e : E U) (k1 : U -> itree E R1) (k2 : U -> itree E R2) : eqit RR b1 b2 (Vis e k1) (Vis e k2) -> forall u, eqit RR b1 b2 (k1 u) (k2 u).
proof: Proof. intros H x; punfold H; apply eqitF_inv_VisF with (x := x) in H; pclearbot; auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)