{motive : Lean.CollectLevelParams.State → Sort u} →
  (t : Lean.CollectLevelParams.State) →
    ((visitedLevel : Lean.LevelSet) →
        (visitedExpr : Lean.ExprSet) →
          (params : Array Lean.Name) →
            motive { visitedLevel := visitedLevel, visitedExpr := visitedExpr, params := params }) →
      motive t