proposition: Theorem trace_eq_iff_eutt : forall {E R} (t1 t2 : itree E R), t1 ≈ t2 <-> trace_eq t1 t2.
proof: Proof. split. - apply eutt_trace_eq. - apply trace_eq_eutt. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)