theorem String.Slice.Pattern.Model.split_char_eq_split_beq {c : Char} {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) : Model.split c f curr hle = Model.split (fun (x : Char) => x == c) f curr hle

theorem String.Slice.toList_splitToSubslice_char {s : Slice} {c : Char} : List.map (copy ∘ Subslice.toSlice) (s.splitToSubslice c).toList = List.map ofList (List.splitOn c s.copy.toList)

theorem String.Slice.toList_split_char {s : Slice} {c : Char} : List.map copy (s.split c).toList = List.map ofList (List.splitOn c s.copy.toList)

theorem String.toList_split_char {s : String} {c : Char} : List.map Slice.copy (s.split c).toList = List.map ofList (List.splitOn c s.toList)

theorem String.Slice.toList_split_intercalate {c : Char} {l : List Slice} (hl : ∀ (s : Slice), s ∈ l → ¬c ∈ s.copy.toList) : List.map copy (((singleton c).toSlice.intercalate l).split c).toList = if l = [] then [""] else List.map copy l

theorem String.Slice.toList_split_intercalate_beq {c : Char} {l : List Slice} (hl : ∀ (s : Slice), s ∈ l → ¬c ∈ s.copy.toList) : ((((singleton c).toSlice.intercalate l).split c).toList == if l = [] then ["".toSlice] else l) = true

theorem String.toList_split_intercalate {c : Char} {l : List String} (hl : ∀ (s : String), s ∈ l → ¬c ∈ s.toList) : List.map (fun (x : Slice) => x.copy) (((singleton c).intercalate l).split c).toList = if l = [] then [""] else l

theorem String.toList_split_intercalate_beq {c : Char} {l : List String} (hl : ∀ (s : String), s ∈ l → ¬c ∈ s.toList) : ((((singleton c).intercalate l).split c).toList == if l = [] then ["".toSlice] else List.map toSlice l) = true