English
There exists a decidable predicate on indices that tests whether the i-th element of the empty list is different from a given element; this predicate is always false.
Русский
Существет decidable-предикат для проверки того, что i-й элемент пустого списка не равен заданному элементу; такой предикат всегда ложно.
LaTeX
$$$$ \\text{decidableGetDNilNe}: \\forall a,\\ \\mathrm{DecidablePred}(\\lambda i: \\mathbb{N}.\\; \\mathrm{getD}([])\\; i\\; a \\neq a). $$$$
Lean4
/-- An empty list can always be decidably checked for the presence of an element.
Not an instance because it would clash with `DecidableEq α`. -/
def decidableGetDNilNe (a : α) : DecidablePred fun i : ℕ => getD ([] : List α) i a ≠ a := fun _ =>
isFalse fun H => H getD_nil
