English
If x : ∀ n, CofixA F n is a coherent family (AllAgree), then the heads of x at height succ n and succ m are equal: head'(x(succ n)) = head'(x(succ m)).
Русский
Если семейство x: ∀ n, CofixA F n согласовано (AllAgree), то головы x на высотах succ n и succ m совпадают: head'(x(succ n)) = head'(x(succ m)).
LaTeX
$$$\\forall F,n,m\\in\\mathbb{N},\\forall x:\\, (\\forall t, CofixA F t)\\, (Hconsistent : \\operatorname{AllAgree} x) ,\\; \\operatorname{head}'(x(\\operatorname{succ} n)) = \\operatorname{head}'(x(\\operatorname{succ} m)).$$$
Lean4
theorem head_succ' (n m : ℕ) (x : ∀ n, CofixA F n) (Hconsistent : AllAgree x) :
head' (x (succ n)) = head' (x (succ m)) :=
by
suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]
clear m n
intro n
rcases h₀ : x (succ n) with - | ⟨_, f₀⟩
cases h₁ : x 1
dsimp only [head']
induction n with
| zero =>
rw [h₁] at h₀
cases h₀
trivial
| succ n n_ih =>
have H := Hconsistent (succ n)
cases h₂ : x (succ n)
rw [h₀, h₂] at H
apply n_ih (truncate ∘ f₀)
rw [h₂]
obtain - | ⟨_, _, hagree⟩ := H
congr
funext j
dsimp only [comp_apply]
rw [truncate_eq_of_agree]
apply hagree
