English
An induction principle for Fix: if p is preserved under Fix.mk with respect to a predicate lift PredLast, then p holds for all x in Fix F α.
Русский
Принцип индукции для Fix: если p сохраняется при Fix.mk относительно предикат-лифты PredLast, тогда p выполняется для всех x в Fix F α.
LaTeX
$$$\forall {p: \mathrm{Fix} F \alpha \to \mathrm{Prop}},\; (\forall x : F (\alpha.append1 (\mathrm{Fix} F \alpha)), \mathrm{LiftP} (PredLast \alpha p) x \to p (\mathrm{Fix.mk} x)) \Rightarrow \forall x, p x$$$
Lean4
theorem ind_aux (a : q.P.A) (f' : q.P.drop.B a ⟹ α) (f : q.P.last.B a → q.P.W α) :
Fix.mk (abs ⟨a, q.P.appendContents f' fun x => ⟦f x⟧⟩) = ⟦q.P.wMk a f' f⟧ :=
by
have : Fix.mk (abs ⟨a, q.P.appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr (q.P.wMk a f' f)⟧ :=
by
apply Quot.sound; apply wEquiv.abs'
rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
conv =>
rhs
rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
congr 2; rw [MvPFunctor.appendContents, MvPFunctor.appendContents]
rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
rfl
rw [this]
apply Quot.sound
apply wrepr_equiv
