English
If b is in dlookup a (kunion l1 l3) and a is not in the keys of l2, then b is in dlookup a ((l1 kunion l2) kunion l3).
Русский
Если b принадлежит dlookup a (kunion l1 l3) и a не принадлежит ключам l2, тогда b принадлежит dlookup a ((l1 kunion l2) kunion l3).
LaTeX
$$$ b \\in dlookup\\ a\\ (l_1\\kunion l_3) \\Rightarrow a \\notin l_2.\\keys \\Rightarrow b \\in dlookup\\ a\\ ((l_1\\kunion l_2)\\kunion l_3) $$$
Lean4
theorem mem_dlookup_kunion_middle {a} {b : β a} {l₁ l₂ l₃ : List (Sigma β)} (h₁ : b ∈ dlookup a (kunion l₁ l₃))
(h₂ : a ∉ keys l₂) : b ∈ dlookup a (kunion (kunion l₁ l₂) l₃) :=
match mem_dlookup_kunion.mp h₁ with
| Or.inl h => mem_dlookup_kunion.mpr (Or.inl (mem_dlookup_kunion.mpr (Or.inl h)))
| Or.inr h => mem_dlookup_kunion.mpr <| Or.inr ⟨mt mem_keys_kunion.mp (not_or.mpr ⟨h.1, h₂⟩), h.2⟩
