English
If two ALists have the same entries up to permutation, inserting the same pair (a, b) into each preserves that permutation relation of their entries.
Русский
Если две AList имеют одни и те же записи до перестановки, вставка одного и того же ключ-значения (a, b) сохраняет это отношение перестановки записями.
LaTeX
$$$ (AList.insert a b s_1).\mathrm{entries} \;\mathrm{Perm}\\ (AList.insert a b s_2).\mathrm{entries} $$$
Lean4
theorem perm_insert {a} {b : β a} {s₁ s₂ : AList β} (p : s₁.entries ~ s₂.entries) :
(insert a b s₁).entries ~ (insert a b s₂).entries := by simp only [entries_insert]; exact p.kinsert s₁.nodupKeys
