English
If j ∈ i :: l and j ≠ i, then the eliminator at j for v ∈ List.TProd α (i :: l) reduces to the tail eliminator at j, i.e., v.elim j = TProd.elim v.2 ((List.mem_cons.mp hj).resolve_left hji).
Русский
Если j принадлежит i :: l и j ≠ i, то элиминация по j для v ∈ List.TProd α (i :: l) равна элиминации хвоста: v.elim j = TProd.elim v.2 (разрешение, что j∈l).
LaTeX
$$$v.\\mathrm{elim}(j\\in i\\!:\\!l) = \\mathrm{TProd}.\\mathrm{elim}\\; v.2\\; ((\\mathrm{List.mem\\_cons.mp}\\; hj).\\mathrm{resolve\_left}\\; hji).$$$
Lean4
@[simp]
theorem elim_of_ne (hj : j ∈ i :: l) (hji : j ≠ i) (v : TProd α (i :: l)) :
v.elim hj = TProd.elim v.2 ((List.mem_cons.mp hj).resolve_left hji) := by simp [TProd.elim, hji]
