English
Extensionality for List.TProd: if l is nodup, and two elements v,w of List.TProd α l agree componentwise on all indices i ∈ l, then v = w.
Русский
Экстенсивность для List.TProd: если l неповторим, и элементы v, w в List.TProd α l согласны по всем индексам i ∈ l, то v = w.
LaTeX
$$$\\forall {l} \\; (l.Nodup) \\to \\forall {v,w : List.TProd α l},\\; (\\forall i \\; (hi : i ∈ l),\\; v.elim hi = w.elim hi) \\to v = w.$$$
Lean4
@[ext]
theorem ext : ∀ {l : List ι} (_ : l.Nodup) {v w : TProd α l} (_ : ∀ (i) (hi : i ∈ l), v.elim hi = w.elim hi), v = w
| [], _, v, w, _ => PUnit.ext v w
| i :: is, hl, v, w, hvw => by
apply Prod.ext
· rw [← elim_self v, hvw, elim_self]
refine ext (nodup_cons.mp hl).2 fun j hj => ?_
rw [← elim_of_mem hl, hvw, elim_of_mem hl]
