English
The multiset of entries is invariant under different parenthesizations of a three-way union: the entries of (s1 ∪ s2 ∪ s3) are a permutation of the entries of (s1 ∪ (s2 ∪ s3)).
Русский
Список элементов объединения трёх AList не зависит от расстановки скобок: entries( s1 ∪ s2 ∪ s3 ) и entries( s1 ∪ (s2 ∪ s3) ) отличаются только перестановкой.
LaTeX
$$$(s_1 \cup s_2 \cup s_3).\text{entries} \sim (s_1 \cup (s_2 \cup s_3)).\text{entries}$$$
Lean4
theorem union_assoc {s₁ s₂ s₃ : AList β} : (s₁ ∪ s₂ ∪ s₃).entries ~ (s₁ ∪ (s₂ ∪ s₃)).entries :=
lookup_ext (AList.nodupKeys _) (AList.nodupKeys _) (by simp [not_or, or_assoc, and_or_left, and_assoc])
