English
If l is nodup, and a is not in l, then replacing a at position n with a yields a nodup list.
Русский
Если список без повторов, и элемент a не встречается в нём, то замена элемента на позиции n на a сохраняет безповторность.
LaTeX
$$$ \\operatorname{Nodup}(l) \\land \\text{a} \\notin l \\Rightarrow \\operatorname{Nodup}(l.\\mathrm{set}\\ n \\ a). $$$
Lean4
protected theorem set : ∀ {l : List α} {n : ℕ} {a : α} (_ : l.Nodup) (_ : a ∉ l), (l.set n a).Nodup
| [], _, _, _, _ => nodup_nil
| _ :: _, 0, _, hl, ha => nodup_cons.2 ⟨mt (mem_cons_of_mem _) ha, (nodup_cons.1 hl).2⟩
| _ :: _, _ + 1, _, hl, ha =>
nodup_cons.2
⟨fun h => (mem_or_eq_of_mem_set h).elim (nodup_cons.1 hl).1 fun hba => ha (hba ▸ mem_cons_self),
hl.of_cons.set (mt (mem_cons_of_mem _) ha)⟩
