∀ (tags : Array Lean.Lsp.CompletionItemTag) (acc : String) (i : ℕ) (h : i < tags.size),
  InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun acc i => tags.size - i)
    ⟨if h_1 : i < tags.size - 1 then acc ++ (tags[i].ctorIdx + 1).repr ++ "," else acc ++ (tags[i].ctorIdx + 1).repr,
      i + 1⟩
    ⟨acc, i⟩