exact ⟨Hs, hz, fun i hi z hiz ↦ by
  rcases h i
    (lt_of_lt_of_le hi (by simp; exact le_trans (lh_bound _) (by simp)))
    ⟨lh s, by simp [lt_succ_iff_le], rfl, by simpa [lt_tsub_iff_right] using hi⟩ z (lt_of_mem_rng hiz) hiz with ⟨_, _, rfl, h⟩
  exact h⟩
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
s : M
Hs : Seq s
h : ∀ i < 2 * s, (∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l) → ∀ z < s, ⟪i, z⟫ ∈ s → ∃ u < s, u = c.succ v i z ∧ ⟪i + 1, u⟫ ∈ s
left✝ : c.zero v < s
hz : ⟪0, c.zero v⟫ ∈ s
⊢ c.CSeq v s
no goals