∀ {b : ByteArray} (hb : 3 ≤ b.size),
  ByteArray.utf8DecodeChar?.parseFirstByte b[0] = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
    b.utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₃ b[0] b[1] b[2]