English
The eta equation for wPathCasesOn: applying wPathCasesOn to its left and right destructors yields the original h.
Русский
Эта лемма-этa для wPathCasesOn: применение к левому и правому деструкторам восстанавливает исходное h.
LaTeX
$$$wPathDestLeft_wPathCasesOn {\alpha} {P} {a} {f} (g' : P.drop.B a ⟹ α) (g : ∀ j, P.WPath (f j) ⟹ α) : P.wPathDestLeft (P.wPathCasesOn g' g) = g'$$$
Lean4
theorem wp_ind {α : TypeVec n} {C : ∀ x : P.last.W, P.WPath x ⟹ α → Prop}
(ih :
∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : P.WPath ⟨a, f⟩ ⟹ α),
(∀ i : P.last.B a, C (f i) (P.wPathDestRight f' i)) → C ⟨a, f⟩ f') :
∀ (x : P.last.W) (f' : P.WPath x ⟹ α), C x f'
| ⟨a, f⟩, f' => ih a f f' fun _i => wp_ind ih _ _
