dlookup_cons_ne — Mathlib

English

If a is not the first component of the head s, then dlookup a (s :: l) = dlookup a l.

Русский

Если a не является первой компонентой головы s, то dlookup a (s :: l) = dlookup a l.

LaTeX

$$$ \\forall l,s:\\; (a \\neq s.1) \\Rightarrow dlookup a (s :: l) = dlookup a l $$$

Lean4

@[simp, grind =]
theorem dlookup_cons_ne (l) {a} : ∀ s : Sigma β, a ≠ s.1 → dlookup a (s :: l) = dlookup a l
  | ⟨_, _⟩, h => dif_neg h.symm

Похожие утверждения