proposition: Lemma sutt_bind' {E R1 R2 S1 S2} {RR: R1 -> R2 -> Prop} {SS: S1 -> S2 -> Prop}: forall t1 t2, sutt RR t1 t2 -> forall s1 s2, (forall r1 r2, RR r1 r2 -> sutt SS (s1 r1) (s2 r2)) -> @sutt E _ _ SS (ITree.bind t1 s1) (ITree.bind t2 s2).
proof: Proof. pcofix self. pstep. intros. punfold H0. unfold observe; cbn. induction H0; intros. - simpl. apply H1 in H. punfold H. eapply monotone_suttF; eauto using upaco2_mon_bot. - simpl. pclearbot. econstructor. eauto with itree. - constructor. eauto with paco. - constructor. pclearbot. right. specialize (self t0 (go ot2) EQTAUS _ _ H1). apply self. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)