@[simp]

theorem String.intercalate_nil {s : String} : s.intercalate [] = ""

@[simp]

theorem String.intercalate_singleton {s t : String} : s.intercalate [t] = t

@[simp]

theorem String.intercalate_cons_cons {s t u : String} {l : List String} : s.intercalate (t :: u :: l) = t ++ s ++ s.intercalate (u :: l)

@[simp]

theorem String.intercalate_cons_append {s t u : String} {l : List String} : s.intercalate ((t ++ u) :: l) = t ++ s.intercalate (u :: l)

theorem String.intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ []) : s.intercalate (t :: l) = t ++ s ++ s.intercalate l

theorem String.intercalate_append_of_ne_nil {l m : List String} {s : String} (hl : l ≠ []) (hm : m ≠ []) : s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m

@[simp]

theorem String.toList_intercalate {s : String} {l : List String} : (s.intercalate l).toList = s.toList.intercalate (List.map toList l)

theorem String.join_eq_foldl {l : List String} : join l = List.foldl (fun (r s : String) => r ++ s) "" l

@[simp]

theorem String.join_nil : join [] = ""

@[simp]

theorem String.join_cons {s : String} {l : List String} : join (s :: l) = s ++ join l

@[simp]

theorem String.toList_join {l : List String} : (join l).toList = List.flatMap toList l

@[simp]

theorem String.appendSlice_eq {s : String} {t : Slice} : s ++ t = s ++ t.copy

@[simp]

theorem String.Slice.intercalate_eq {s : Slice} {l : List Slice} : s.intercalate l = s.copy.intercalate (List.map copy l)

@[simp]

theorem String.Slice.join_eq {l : List Slice} : join l = String.join (List.map copy l)