English
Characterization of membership in a cons-constructed Sym2: z ∈ (x :: xs).sym2 if and only if z equals s(x,x) or z equals s(x,y) for some y ∈ xs or z ∈ xs.sym2.
Русский
Характеризация принадлежности элемента z сим2 списка (x :: xs): z = s(x,x) или z = s(x,y) для некоторого y ∈ xs, или z ∈ xs.sym2.
LaTeX
$$$$ z \\in (x :: xs).sym2 \\quad\\Leftrightarrow\\quad z = s(x,x) \\;\\lor\\; (\\exists y \\; (y \\in xs \\land z = s(x,y))) \\;\\lor\\; z \\in xs.sym2 $$$$
Lean4
theorem mem_sym2_cons_iff {x : α} {xs : List α} {z : Sym2 α} :
z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y, y ∈ xs ∧ z = s(x, y)) ∨ z ∈ xs.sym2 :=
by
simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]
simp only [eq_comm]
