English
If a list l has no duplicate keys, then kerase a l also has no duplicate keys. In particular, kerase preserves the nodup-key property.
Русский
Если у списка l нет повторяющихся ключей, то и kerase a l не имеет повторяющихся ключей. kerase сохраняет свойство без повторов ключей.
LaTeX
$$∀ {a} (nd : l.NodupKeys), (kerase a l).NodupKeys$$
Lean4
theorem kerase (a : α) : NodupKeys l → (kerase a l).NodupKeys :=
NodupKeys.sublist <| kerase_sublist _ _