English
There is an induction principle for W: if for every constructor a with tail f′ and subtrees f, C holds whenever it holds for all subtrees, then C holds for every W-tree.
Русский
Существует индукционный принцип для W: если для каждого конструктора a с хвостом f′ и поддеревьями f верно C при условии верности C для всех поддеревьев, тогда C верно для каждого дерева W.
LaTeX
$$$\forall x,\, C\,x\quad\text{where } C:\, P.W\,\alpha \to \text{Prop},\ \text{and }\, (\forall a\, f'\, f,\ (\forall i, C(f\, i)) \to C(wMk\, a\, f'\, f)).$$$
Lean4
/-- Induction principle for `W` -/
theorem w_ind {α : TypeVec n} {C : P.W α → Prop}
(ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ i, C (f i)) → C (P.wMk a f' f)) : ∀ x, C x :=
by
intro x; obtain ⟨a, f⟩ := x
apply @wp_ind n P α fun a f => C ⟨a, f⟩
intro a f f' ih'
dsimp [wMk] at ih
let ih'' := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
dsimp at ih''; rw [wPathCasesOn_eta] at ih''
apply ih''
apply ih'
