consCases_cons — Mathlib

English

Applying consCases to a cons-constructed input is the same as applying h to the head and tail: consCases h (cons x0 x) = h x0 x.

Русский

Применение consCases к cons-образному вхождению равно применению h к голове и хвосту: consCases h (cons x0 x) = h x0 x.

LaTeX

$$$\\\\mathrm{consCases}\\, h\\ (\\\\mathrm{cons} x_0 x) = h\\ x_0 x$$$

Lean4

@[simp]
theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x)) (x₀ : α 0)
    (x : ∀ i : Fin n, α i.succ) : consCases h (cons x₀ x) = h x₀ x :=
  by
  rw [consCases, cast_eq]
  congr

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