English
For xs and x, xs is an infix of [x] if and only if xs is empty or xs = [x].
Русский
Для xs и x, xs является инфиксом [x] тогда и только тогда, когда xs пуст, или xs = [x].
LaTeX
$$$\forall {\alpha},\ xs:\, \text{List}(\alpha),\ x:\, \alpha,\; xs <:+: [x] \iff xs = \emptyset \text{ or } xs = [x].$$$
Lean4
theorem infix_singleton_iff (xs : List α) (x : α) : xs <:+: [x] ↔ xs = [] ∨ xs = [x] := by
match xs with
| [] => simp
| [_] => simp [List.singleton_infix_singleton_iff]
| _ :: _ :: _ =>
constructor
· rintro ⟨_ | _, _, h⟩ <;> simp at h
· simp