English
If a ≠ a', then the two insert steps commute up to permutation of entries: the two resulting lists of entries are permutation-equivalent.
Русский
Если a ≠ a', то два шага вставки совместимы до перестановки записей: итоговые списки записей эквивалентны по перестановке.
LaTeX
$$$ a
eq a' \Rightarrow ((s.insert a b).insert a' b').entries \\text{Perm} ((s.insert a' b').insert a b).entries $$$
Lean4
theorem insert_insert_of_ne {a a'} {b : β a} {b' : β a'} (s : AList β) (h : a ≠ a') :
((s.insert a b).insert a' b').entries ~ ((s.insert a' b').insert a b).entries := by simp only [entries_insert];
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;> [apply Perm.swap; exact h; exact h.symm]
