English
Let a family C: ℕ → Sort*, n ≤ m, and a forward-step function next with each next injective; then the recursor leRecOn is injective from C n to C m.
Русский
Пусть C: ℕ → Sort*, n ≤ m, и есть функция перехода next с инъективными переходами; тогда рекурсор leRecOn инъективен на отображении C n → C m.
LaTeX
$$$\text{Injective}(\mathrm{leRecOn}\ C\ n\ m\ hnm\ next)$$$
Lean4
theorem leRecOn_injective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
(Hnext : ∀ n, Injective (@next n)) : Injective (@leRecOn C n m hnm next) := by
induction hnm with
| refl =>
intro x y H
rwa [leRecOn_self, leRecOn_self] at H
| step hnm ih =>
intro x y H
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
exact ih (Hnext _ H)
