fact: Fixpoint trace_ret {E R} (tr : @trace E R) : option R := match tr with | TRet r => (Some r) | TEventResponse _ _ tr => trace_ret tr | _ => None end.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)