proposition: Theorem eutt_sutt {E R1 R2} (RR : R1 -> R2 -> Prop) : forall (t1 : itree E R1) (t2 : itree E R2), eutt RR t1 t2 -> sutt RR t1 t2.
proof: Proof. pcofix CIH. pstep. intros. punfold H0. red in H0. induction H0; constructor; pclearbot; eauto 7 with paco itree. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)