English
The induction principle for Fix F: if p is a property of Fix F and holds for Fix.mk x whenever it holds for x in F(Fix F) (lifted appropriately), then p holds for all Fix F.
Русский
Принцип индукции для Fix F: если свойство p верно для Fix F и выполняется для Fix.mk x при условии, что p верно для x в F(Fix F) (со смещением через Liftp), то p выполняется для всех Fix F.
LaTeX
$$$$\forall {F : Type u \to Type v} [q : QPF F] (p : Fix F \to Prop), (h : \forall x : F (Fix F), Liftp p x \to p (Fix.mk x)) \rightarrow \forall x, p x.$$$$
Lean4
theorem ind (p : Fix F → Prop) (h : ∀ x : F (Fix F), Liftp p x → p (Fix.mk x)) : ∀ x, p x :=
by
rintro ⟨x⟩
induction x with
| _ a f ih
change p ⟦⟨a, f⟩⟧
rw [← Fix.ind_aux a f]
apply h
rw [liftp_iff]
refine ⟨_, _, rfl, ?_⟩
convert ih
