trList_ne_consₗ — Mathlib

English

No element of trList(l) equals the distinguished symbol consₗ; every member is different from Γ'.consₗ.

Русский

Никакой элемент из trList(l) не равен обозначению consₗ; каждый элемент отличается от Γ'.consₗ.

LaTeX

$$$\\forall \\ell, \\forall x \\in \\operatorname{trList}(\\ell),\n x \\neq \\Gamma'.\\text{cons}_{\\ell}$$$

Lean4

theorem trList_ne_consₗ : ∀ (l), ∀ x ∈ trList l, x ≠ Γ'.consₗ
  | a :: l, x, h => by
    simp only [trList, List.mem_append, List.mem_cons] at h
    obtain h | rfl | h := h
    · rintro rfl
      cases trNat_natEnd _ _ h
    · rintro ⟨⟩
    · exact trList_ne_consₗ l _ h

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