∀ (suggestions : Array Lean.Name) (_x : (_ : ℕ) ×' (_ : Array Lean.Name) ×' Lean.LocalContext),
  Aesop.getUnusedNames.go._unary✝ suggestions _x =
    PSigma.casesOn _x fun i acc =>
      PSigma.casesOn acc fun acc lctx =>
        if h : i < suggestions.size then
          have name := lctx.getUnusedName suggestions[i];
          have lctx := lctx.addDecl (Aesop.getUnusedNames.dummyLDecl✝ name);
          Aesop.getUnusedNames.go._unary✝¹ suggestions ⟨i + 1, ⟨acc.push name, lctx⟩⟩
        else (acc, lctx)