∀ (w x y z : UInt8),
  ByteArray.utf8DecodeChar?.verify₄ w x y z =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
              ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
          true then
      false
    else
      have r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
      decide (65536 ≤ r ∧ r ≤ 1114111)