∀ (c : Char) (motive : List UInt8 → Prop),
  (have v := c.val.toNat;
    v ≤ 127 → motive [UInt8.ofNat v]) →
    (have v := c.val.toNat;
      ¬v ≤ 127 → v ≤ 2047 → motive [UInt8.ofNat (v / 64 % 32 + 192), UInt8.ofNat (v % 64 + 128)]) →
      (have v := c.val.toNat;
        ¬v ≤ 127 →
          ¬v ≤ 2047 →
            v ≤ 65535 →
              motive [UInt8.ofNat (v / 4096 % 16 + 224), UInt8.ofNat (v / 64 % 64 + 128), UInt8.ofNat (v % 64 + 128)]) →
        (have v := c.val.toNat;
          ¬v ≤ 127 →
            ¬v ≤ 2047 →
              ¬v ≤ 65535 →
                motive
                  [UInt8.ofNat (v / 262144 % 8 + 240), UInt8.ofNat (v / 4096 % 64 + 128),
                    UInt8.ofNat (v / 64 % 64 + 128), UInt8.ofNat (v % 64 + 128)]) →
          motive (String.utf8EncodeChar c)