fact: Definition step {E : Type -> Type} {R : Type} (ev : event E) (t t' : itree E R) : Prop := step_ ev t' t.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)