English
A case analysis on WPath: to define a function on WPath ⟨a,f⟩ ⟹ α, it is enough to provide a function on the root case and on the child cases with appropriate compatibility.
Русский
Разбор случаев на WPath: чтобы определить функцию на WPath ⟨a,f⟩ ⟹ α, достаточно задать функцию на корневом случае и на случаи потомков с необходимой совместимостью.
LaTeX
$$$wPathCasesOn : (α) (a,f) → (⋯) → WPath ⟨a,f⟩ ⟹ α$$$
Lean4
theorem wpRec_eq {α : TypeVec n} {C : Type*}
(g : ∀ (a : P.A) (f : P.last.B a → P.last.W), P.WPath ⟨a, f⟩ ⟹ α → (P.last.B a → C) → C) (a : P.A)
(f : P.last.B a → P.last.W) (f' : P.WPath ⟨a, f⟩ ⟹ α) :
P.wpRec g ⟨a, f⟩ f' = g a f f' fun i => P.wpRec g (f i) (P.wPathDestRight f' i) :=
rfl
