∀ (items : Array Lean.Lsp.ResolvableCompletionItem) (acc : String) (i : ℕ) (h : i < items.size),
  InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun acc i => items.size - i)
    ⟨if h_1 : i < items.size - 1 then Lean.Lsp.ResolvableCompletionList.compressItemFast✝ acc items[i] ++ ","
      else Lean.Lsp.ResolvableCompletionList.compressItemFast✝¹ acc items[i],
      i + 1⟩
    ⟨acc, i⟩