∀ (s : String.Slice) (_x : (offset : String.Pos.Raw) ×' offset ≤ s.rawEndPos),
  String.Slice.posGE._unary s _x =
    PSigma.casesOn _x fun offset h =>
      if h' : String.Pos.Raw.IsValidForSlice s offset then s.pos offset h'
      else
        have this := ⋯;
        String.Slice.posGE._unary s ⟨offset.inc, ⋯⟩