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