English
If a is in the keys of l1, then looking up a in kunion(l1,l2) yields the same as looking up a in l1.
Русский
Если a принадлежит ключам l1, то поиск a в kunion(l1,l2) равен поиску a в l1.
LaTeX
$$$ a \\in l_1.\\keys \\Rightarrow dlookup(a,kunion(l_1,l_2)) = dlookup(a,l_1) $$$
Lean4
@[simp]
theorem dlookup_kunion_left {a} {l₁ l₂ : List (Sigma β)} (h : a ∈ l₁.keys) : dlookup a (kunion l₁ l₂) = dlookup a l₁ :=
by
induction l₁ generalizing l₂ with
| nil => simp at h
| cons s _ ih =>
simp only [keys_cons, mem_cons] at h
rcases h with rfl | h <;> obtain ⟨a'⟩ := s
· simp
· rw [kunion_cons]
by_cases h' : a = a'
· subst h'
simp
· simp [h', ih h]