{α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type u_1} →
        [Monad m] →
          ((a : α) → β a → δ → m δ) →
            (x : Std.DTreeMap.Internal.Impl α β) →
              Std.DTreeMap.Internal.Impl.below (motive := fun x => δ → m δ) x → δ → m δ