fact: Definition is_trace {E : Type -> Type} {R : Type} (t : itree E R) := is_traceF (observe t).
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)