proposition: Lemma eqit_Vis b1 b2 {U} (e : E U) (k1 : U -> itree E R1) (k2 : U -> itree E R2) : (forall u, eqit RR b1 b2 (k1 u) (k2 u)) -> eqit RR b1 b2 (Vis e k1) (Vis e k2).
proof: Proof. apply eqit_Vis_gen with (p := eq_refl); constructor. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)