∀ {p : Char → Bool}
  (motive :
    ((∃ x ∈ List.finRange Char.minSurrogate, p (Char.ofNatAux ↑x ⋯) = true) ∨
        ∃ x ∈ List.finRange (Char.max - Char.maxSurrogate), p (Char.ofNatAux (↑x + Char.maxSurrogate + 1) ⋯) = true) →
      Prop)
  (h :
    (∃ x ∈ List.finRange Char.minSurrogate, p (Char.ofNatAux ↑x ⋯) = true) ∨
      ∃ x ∈ List.finRange (Char.max - Char.maxSurrogate), p (Char.ofNatAux (↑x + Char.maxSurrogate + 1) ⋯) = true),
  (∀ (n : ℕ) (hn : n < Char.minSurrogate) (left : ⟨n, hn⟩ ∈ List.finRange Char.minSurrogate)
      (h : p (Char.ofNatAux ↑⟨n, hn⟩ ⋯) = true), motive ⋯) →
    (∀ (n : ℕ) (isLt : n < Char.max - Char.maxSurrogate)
        (left : ⟨n, isLt⟩ ∈ List.finRange (Char.max - Char.maxSurrogate))
        (h : p (Char.ofNatAux (↑⟨n, isLt⟩ + Char.maxSurrogate + 1) ⋯) = true), motive ⋯) →
      motive h