typevecCasesCons₂_appendFun — Mathlib

English

For all n, t, t', v, v', a function F, and elements f, fs, we have the equality: typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs.

Русский

Для всех n, t, t', v, v' и функции F, а также элементов f, fs выполняется равенство: typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs.

LaTeX

$$$$\\forall n\\, t\\, t'\\, v\\, v'\\, (F)\\, (f)\\, (fs),\\; \\text{typevecCasesCons₂ } n t t' v v' F (fs ::: f) = F f fs.$$$$

Lean4

theorem typevecCasesCons₂_appendFun (n : ℕ) (t t' : Type*) (v v' : TypeVec n) {β : (v ::: t) ⟹ (v' ::: t') → Sort*}
    (F : ∀ (f : t → t') (fs : v ⟹ v'), β (fs ::: f)) (f fs) : typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs :=
  rfl

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