fact: Definition subst {E : Type -> Type} {T U : Type} (k : T -> itree E U) : itree E T -> itree E U := cofix _subst (u : itree E T) : itree E U := match observe u with | RetF r => k r | TauF t => Tau (_subst t) | VisF e h => Vis e (fun x => _subst (h x)) end.
imports: ExtLib.Structures.Functor ExtLib.Structures.Applicative ExtLib.Structures.Monad Program.Tactics ITree(Basics)