English
Permuting the underlying list preserves the kreplace operation up to permutation: if l1 ~ l2, then kreplace a b l1 ~ kreplace a b l2.
Русский
Перестановка базового списка сохраняет операцию kreplace до перестановки: если l1 ~ l2, то kreplace a b l1 ~ kreplace a b l2.
LaTeX
$$$ l_1 \sim l_2 \rightarrow \mathrm{Perm}(\mathrm{kreplace}(a,b,l_1),\mathrm{kreplace}(a,b,l_2)) $$$
Lean4
theorem kreplace {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys) :
l₁ ~ l₂ → kreplace a b l₁ ~ kreplace a b l₂ :=
perm_lookmap _ <| by
refine nd.pairwise_ne.imp ?_
intro x y h z h₁ w h₂
split_ifs at h₁ h₂ with h_2 h_1 <;> cases h₁ <;> cases h₂
exact (h (h_2.symm.trans h_1)).elim
