English
Let n be a natural number. For any C : TypeVec (n+1) → Type and any H : ∀ α β, C (append1 α β), the value of the case analysis on the append1-constructor is exactly the prescribed value: append1Cases H (append1 α β) = H α β.
Русский
Пусть n натурально число. Пусть C : TypeVec (n+1) → Type, и H : ∀ α β, C (append1 α β). Тогда значение разборки конструктора append1 на α, β равно заданному: append1Cases H (append1 α β) = H α β.
LaTeX
$$$\forall n\,\forall C:\, TypeVec(n+1)\to\text{Type},\ \forall H:\forall \alpha:TypeVec\ n,\forall \beta:\text{Type},\append1Cases\ H\ (\append1\alpha\beta)=H\alpha\beta$$$
Lean4
@[simp]
theorem append1_cases_append1 {C : TypeVec (n + 1) → Sort u} (H : ∀ α β, C (append1 α β)) (α β) :
@append1Cases _ C H (append1 α β) = H α β :=
rfl
