casesCons_append1 — Mathlib

English

For every n, every β, v, and α, the equality TypeVec.casesCons n f (v ::: α) = f α v holds, expressing the compatibility of the constructor with the append operation.

Русский

Для каждого n, β, v и α выполняется равенство TypeVec.casesCons n f (v ::: α) = f α v, выражающее совместимость конструктора с операцией дополнения.

LaTeX

$$$$\\mathrm{TypeVec.casesCons}\\ n\\ f\\ (v ::: \\alpha) = f\\alpha\\,v.$$$$

Lean4

protected theorem casesCons_append1 (n : ℕ) {β : TypeVec (n + 1) → Sort*} (f : ∀ (t) (v : TypeVec n), β (v ::: t))
    (v : TypeVec n) (α) : TypeVec.casesCons n f (v ::: α) = f α v :=
  rfl

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