theorem List.eq_of_append_eq (s₁ s₂ t₁ t₂ : List Char) (le : String.utf8Len s₁ ≤ String.utf8Len t₁) (eq : s₁ ++ s₂ = t₁ ++ t₂) : ∃ (u : List Char), s₁ ++ u = t₁ ∧ s₂ = u ++ t₂

theorem String.eq_of_append_eq {s₁ s₂ t₁ t₂ : String} (le : s₁.utf8ByteSize ≤ t₁.utf8ByteSize) (eq : s₁ ++ s₂ = t₁ ++ t₂) : ∃ (u : String), s₁ ++ u = t₁ ∧ s₂ = u ++ t₂

theorem String.empty_or_eq_singleton_append (s : String) : s = "" ∨ ∃ (c : Char), ∃ (t : String), s = singleton c ++ t

theorem String.ValidPos.find_le_pos {s : String} {pos : s.ValidPos} {p : Char → Bool} : pos ≤ pos.find p

theorem String.ValidPos.find_soundness {s : String} {pos : s.ValidPos} {p : Char → Bool} : (∃ (h : pos.find p ≠ s.endValidPos), p ((pos.find p).get h) = true) ∨ pos.find p = s.endValidPos

theorem String.ValidPos.find_completenessAux {s : String} {pos : s.ValidPos} (p : Char → Bool) {l mr : String} (sp : pos.Splits l mr) : ∃ (m : String), ∃ (r : String), (pos.find p).Splits (l ++ m) r ∧ ∀ (c : Char), m.contains c = true → ¬p c = true

theorem String.ValidPos.find_completeness {s : String} {pos pos' : s.ValidPos} {p : Char → Bool} (ge : pos ≤ pos') (lt : pos' < pos.find p) : ¬p (pos'.get ⋯) = true