proposition: Lemma eutt_trace_eq : forall {E R} (t1 t2 : itree E R), t1 ≈ t2 -> trace_eq t1 t2.
proof: Proof. split. - apply sutt_trace_incl; apply eutt_sutt; auto. - symmetry in H. apply sutt_trace_incl; apply eutt_sutt; auto. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)