proposition: Lemma sutt_tau_right {E R1 R2} (RR : R1 -> R2 -> Prop) : forall (t1 : itree E R1) (t2 : itree E R2), sutt RR t1 t2 -> sutt RR t1 (Tau t2).
proof: Proof. intros. punfold H. pstep. repeat red. repeat red in H. constructor. auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)