proposition: Lemma rutt_bind {E1 E2 R1 R2 T1 T2} (REv: forall A B, E1 A -> E2 B -> Prop) (RAns: forall A B, E1 A -> A -> E2 B -> B -> Prop) (RR: R1 -> R2 -> Prop) (RT: T1 -> T2 -> Prop) t1 t2 k1 k2: rutt REv RAns RR t1 t2 -> (forall r1 r2, RR r1 r2 -> rutt REv RAns RT (k1 r1) (k2 r2)) -> rutt REv RAns RT (ITree.bind t1 k1) (ITree.bind t2 k2).
proof: Proof. intros. ginit. eapply gpaco2_uclo; [|eapply rutt_clo_bind|]; eauto with paco. econstructor; eauto. intros; subst. gfinal. right. apply H0. eauto. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)