English
Let α be a type and β a family of types over α with a decidable equality on α. For AList β and any a ∈ α, b ∈ β a, and s1, s2 : AList β, inserting the pair (a,b) into the union s1 ∪ s2 is the same as first inserting into s1 and then taking the union with s2; i.e. insert a b (s1 ∪ s2) = insert a b s1 ∪ s2.
Русский
Пусть α — множество, β — семейство множеств над α, выполнено сравнение по α. Для AList β и любых a ∈ α, b ∈ β a, а также s1, s2 : AList β, вставка пары (a,b) в объединение s1 ∪ s2 равна объединению вставки в s1 с s2; то есть insert a b (s1 ∪ s2) = insert a b s1 ∪ s2.
LaTeX
$$$AList.insert\ a\ b\ (AList.instUnion.union\ s_1\ s_2) = AList.instUnion.union\ (AList.insert\ a\ b\ s_1)\ s_2$$$
Lean4
theorem insert_union {a} {b : β a} {s₁ s₂ : AList β} : insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂ := by ext; simp
