∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match ByteArray.utf8DecodeChar?.FirstByte.done with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 ()
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 ()
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 ()
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 ()
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 ()) =
    h_2 ()