∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.forIn f init t = do
    let __do_lift ← Std.DTreeMap.Internal.Impl.forInStep f init t
    match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => pure d