English
A dependent induction principle for Fix: given a family g over Fix.mk-constructed elements, if for all x the corresponding equality holds after lifting with appendFun, then for each x in Fix F α, the property holds.
Русский
Зависимый принцип индукции для Fix: если для всех x верно неравенство после лифтинга с appendFun, то свойство выполняется для всех x.
LaTeX
$$$\forall {n} {F} [q : MvQPF F] {\alpha} {\beta}, \; (g : \forall x : F (\alpha ::: Sigma \beta), \beta (Fix.mk x)) \Rightarrow (x : Fix F \alpha) \Rightarrow g x$$$
Lean4
theorem ind_rec {β : Type u} (g₁ g₂ : Fix F α → β)
(h :
∀ x : F (append1 α (Fix F α)), appendFun id g₁ <$$> x = appendFun id g₂ <$$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)) :
∀ x, g₁ x = g₂ x := by
apply Quot.ind
intro x
apply q.P.w_ind _ x
intro a f' f ih
change g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧
rw [← Fix.ind_aux a f' f]
apply h
rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
congr 2
rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
have : (g₁ ∘ fun x => ⟦f x⟧) = g₂ ∘ fun x => ⟦f x⟧ := by
ext x
exact ih x
rw [this]
