English
If a ≠ a' then dlookup a (kerase a' l) = dlookup a l. The entry for a is unaffected when erasing a' unless a equals a'.
Русский
Если a ≠ a', то dlookup a (kerase a' l) = dlookup a l. Удаление элемента с ключом a' не повлияет на запись a.
LaTeX
$$∀ {a a'} {l : List (Σ β)} (h : a ≠ a'), dlookup a (kerase a' l) = dlookup a l$$
Lean4
@[simp]
theorem dlookup_kerase_ne {a a'} {l : List (Sigma β)} (h : a ≠ a') : dlookup a (kerase a' l) = dlookup a l := by
induction l with
| nil => rfl
| cons hd tl ih =>
obtain ⟨ah, bh⟩ := hd
by_cases h₁ : a = ah <;> by_cases h₂ : a' = ah
· substs h₁ h₂
cases Ne.irrefl h
· subst h₁
simp [h₂]
· subst h₂
simp [h]
· simp [h₁, h₂, ih]
