English
For any a, lookupAll a l equals the empty list iff no element of l has first component a.
Русский
Для любого a lookupAll a l равно пустому списку тогда и только тогда, когда в l нет элемента с первой координатой a.
LaTeX
$$$ \lookupAll a l = \emptyset \\iff \forall b, \langle a,b\rangle \notin l $$$
Lean4
theorem lookupAll_eq_nil {a : α} : ∀ {l : List (Sigma β)}, lookupAll a l = [] ↔ ∀ b : β a, Sigma.mk a b ∉ l
| [] => by simp
| ⟨a', b⟩ :: l => by
by_cases h : a = a'
· subst a'
simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or, false_iff, not_forall,
not_and, not_not, reduceCtorEq]
use b
simp
· simp [h, lookupAll_eq_nil]
