English
An alternative induction principle for Fix that mirrors the previous ind, using PredLast and LiftP to carry the predicate through Fix.mk.
Русский
Альтернативный принцип индукции для Fix; переносит предикат через Fix.mk с помощью PredLast и LiftP.
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 {α : TypeVec n} (p : Fix F α → Prop)
(h : ∀ x : F (α.append1 (Fix F α)), LiftP (PredLast α p) x → p (Fix.mk x)) : ∀ x, p x :=
by
apply Quot.ind
intro x
apply q.P.w_ind _ x; intro a f' f ih
change p ⟦q.P.wMk a f' f⟧
rw [← Fix.ind_aux a f' f]
apply h
rw [MvQPF.liftP_iff]
refine ⟨_, _, rfl, ?_⟩
intro i j
cases i
· apply ih
· trivial
