proposition: Lemma trace_eq_eutt : forall {E R} (t1 t2 : itree E R), trace_eq t1 t2 -> t1 ≈ t2.
proof: Proof. intros E R t1 t2 [? ?]. apply sutt_eutt. - apply trace_incl_sutt; auto. - apply trace_incl_sutt in H0. clear H. generalize dependent t1. generalize dependent t2. pcofix CIH; pstep; intros. punfold H0. induction H0; constructor; try red; pclearbot; eauto with paco itree. right. rewrite itree_eta'. eauto with paco itree. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)