{α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] →
            [LawfulMonad m] → [Std.TransCmp cmp] → (δ → (a : α) → β a → m δ) → δ → Std.ExtDTreeMap α β cmp → m δ