fact: Definition trace_eq {E : Type -> Type} {R : Type} : itree E R -> itree E R -> Prop := fun t1 t2 => trace_incl t1 t2 /\ trace_incl t2 t1.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)