{m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    {α : Type} →
      [Monad m] →
        [Inhabited σ] →
          (σ → α → m σ) →
            (α → m (ULift.{u_1, 0} Bool)) → σ → Lean.Meta.DiscrTree.Trie α → m (Lean.Meta.DiscrTree.Trie α × σ)