∀ {c : Char},
  c.val < 55295 →
    ∀ (h : ¬c.val < 55296) (_x_1 : ↑c.ordinal + 1 < Char.numCodePoints),
      c.val + 1 =
        if h_1 : c.val.toNat - 2048 + 1 < 55296 then UInt32.ofNatLT (c.val.toNat - 2048) ⋯ + 1
        else UInt32.ofNatLT (c.val.toNat - 2048) ⋯ + 1 + UInt32.ofNatLT 2048 ⋯