proposition: Lemma sutt_elim_tau_right {E R1 R2} (RR : R1 -> R2 -> Prop) : forall (t1: itree E R1) (t2: itree E R2), sutt RR t1 (Tau t2) -> sutt RR t1 t2.
proof: Proof. pcofix CIH. pstep. intros. punfold H0. repeat red in H0. inv H0. - eapply monotone_suttF; eauto using upaco2_mon_bot with paco. - constructor. pclearbot. eauto with paco. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)