fact: Definition interp_mrec {D E : Type -> Type} (ctx : D ~> itree (D +' E)) : itree (D +' E) ~> itree E := fun R => ITree.iter (fun t : itree (D +' E) R => match observe t with | RetF r => Ret (inr r) | TauF t => Ret (inl t) | VisF (inl1 d) k => Ret (inl (ctx _ d >>= k)) | VisF (inr1 e) k => Vis e (fun x => Ret (inl (k x))) end).
imports: ITree(Basics.Basics Basics.Category Core.ITreeDefinition Indexed.Sum)