∀ (c : Char) (motive : ℕ → Prop),
  (have v := c.val;
    v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 → motive 1) →
    (have v := c.val;
      ¬v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 → v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 → motive 2) →
      (have v := c.val;
        ¬v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 →
          ¬v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 →
            v ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 → motive 3) →
        (have v := c.val;
          ¬v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 →
            ¬v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 →
              ¬v ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 → motive 4) →
          motive c.utf8Size