English
For v ∈ List.TProd α (i :: l), the eliminator at the position mem_cons_self yields the first component, i.e., v.elim mem_cons_self = v.1.
Русский
Для v ∈ List.TProd α (i :: l) элиминация по mem_cons_self дает первую компоненту: v.elim mem_cons_self = v.1.
LaTeX
$$$(v\\,\\text{elim}\\ text{ mem\\_cons\\_self}) = v.\\mathrm{fst}.$$$
Lean4
@[simp]
theorem elim_self (v : TProd α (i :: l)) : v.elim mem_cons_self = v.1 := by simp [TProd.elim]