∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos}
  (motive :
    (∃ c,
        (∃ t₂,
            ∃ (h : s.startPos ≠ s.endPos),
              pos = s.startPos.next h ∧ s.startPos.get h = c ∧ s.copy = String.singleton c ++ t₂) ∧
          p c = true) →
      Prop)
  (x :
    ∃ c,
      (∃ t₂,
          ∃ (h : s.startPos ≠ s.endPos),
            pos = s.startPos.next h ∧ s.startPos.get h = c ∧ s.copy = String.singleton c ++ t₂) ∧
        p c = true),
  (∀ (c : Char) (t₂ : String) (h : s.startPos ≠ s.endPos) (h₁ : pos = s.startPos.next h) (h₂ : s.startPos.get h = c)
      (h₃ : s.copy = String.singleton c ++ t₂) (hc : p c = true), motive ⋯) →
    motive x