proposition: Lemma eqit_Vis_gen b1 b2 {U1 U2} (p : U1 = U2) (e1 : E U1) (e2 : E U2) (k1 : U1 -> itree E R1) (k2 : U2 -> itree E R2) : eqeq E p e1 e2 -> pweqeq (eqit RR b1 b2) p k1 k2 -> eqit RR b1 b2 (Vis e1 k1) (Vis e2 k2).
proof: Proof. destruct p; cbn. intros <- H. pstep. econstructor. left. apply H. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)