proposition: Lemma eqit_bind' {E R1 R2 S1 S2} (RR : R1 -> R2 -> Prop) b1 b2 (RS : S1 -> S2 -> Prop) t1 t2 k1 k2 : eqit RR b1 b2 t1 t2 -> (forall r1 r2, RR r1 r2 -> eqit RS b1 b2 (k1 r1) (k2 r2)) -> @eqit E _ _ RS b1 b2 (ITree.bind t1 k1) (ITree.bind t2 k2).
proof: Proof. intros. ginit. guclo eqit_clo_bind. unfold eqit in *. econstructor; eauto with paco. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)