@[simp]

theorem String.Slice.contains_slice_iff {t s : Slice} : s.contains t = true ↔ t.copy.toList <:+: s.copy.toList

@[simp]

theorem String.Slice.contains_string_iff {t : String} {s : Slice} : s.contains t = true ↔ t.toList <:+: s.copy.toList

@[simp]

theorem String.Slice.contains_slice_eq_false_iff {t s : Slice} : s.contains t = false ↔ ¬t.copy.toList <:+: s.copy.toList

@[simp]

theorem String.Slice.contains_string_eq_false_iff {t : String} {s : Slice} : s.contains t = false ↔ ¬t.toList <:+: s.copy.toList

@[simp]

theorem String.contains_slice_iff {t : Slice} {s : String} : s.contains t = true ↔ t.copy.toList <:+: s.toList

@[simp]

theorem String.contains_string_iff {t s : String} : s.contains t = true ↔ t.toList <:+: s.toList

@[simp]

theorem String.contains_slice_eq_false_iff {t : Slice} {s : String} : s.contains t = false ↔ ¬t.copy.toList <:+: s.toList

@[simp]

theorem String.contains_string_eq_false_iff {t s : String} : s.contains t = false ↔ ¬t.toList <:+: s.toList

theorem String.contains_string_eq_internal {t s : String} : s.contains t = t.toList.isInfixOf_internal s.toList