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