fact: Definition translate {E F} (h : E ~> F) : itree E ~> itree F := fun R => cofix translate_ t := translateF h translate_ (observe t).
imports: ExtLib(Structures.Functor Structures.Monad) ITree(Basics.Basics Core.ITreeDefinition Indexed.Relation)