English
If a ∈ l (with nodup keys), then a is not present in (kerase a l).keys. Erasing a from the list removes its key from the key-set.
Русский
Если ключ a присутствует в l с безповторными ключами, то a не принадлежит (kerase a l).keys.
LaTeX
$$∀ {l : List (Σ β)}, l.NodupKeys → a ∉ (kerase a l).keys$$
Lean4
theorem sizeOf_kerase [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) :
SizeOf.sizeOf (List.kerase x xs) ≤ SizeOf.sizeOf xs :=
by
simp only [SizeOf.sizeOf, _sizeOf_1]
induction xs with
| nil => simp
| cons y ys => by_cases x = y.1 <;> simp [*]