English
If s1 ~ s2 and s3 ~ s4, then (s1 ∪ s3) ~ (s2 ∪ s4).
Русский
Если записи s1 и s2 равны (помечены как Perm), и записи s3 и s4 равны, то объединение также сохраняет соответствие по перестановке.
LaTeX
$$$ s_1.\mathrm{entries} \;\mathrm{Perm} \; s_2.\mathrm{entries} \Rightarrow s_3.\mathrm{entries} \;\mathrm{Perm} \; s_4.\mathrm{entries} \Rightarrow (s_1 \cup s_3).\mathrm{entries} \;\mathrm{Perm} \; (s_2 \cup s_4).\mathrm{entries} $$$
Lean4
theorem perm_union {s₁ s₂ s₃ s₄ : AList β} (p₁₂ : s₁.entries ~ s₂.entries) (p₃₄ : s₃.entries ~ s₄.entries) :
(s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries := by simp [p₁₂.kunion s₃.nodupKeys p₃₄]
