exact ⟨lt_of_mem_rng this, rfl, this⟩
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
hz : ⟪0, c.zero v⟫ ∈ s
hs : ∀ i < lh s - 1, ∀ (z : M), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s
i : M
x✝¹ : i < 2 * s
hi : ∃ l ≤ 2 * s, l = lh s ∧ i + 1 < l
z : M
x✝ : z < s
hiz : ⟪i, z⟫ ∈ s
this : ⟪i + 1, c.succ v i z⟫ ∈ s
⊢ c.succ v i z < s ∧ c.succ v i z = c.succ v i z ∧ ⟪i + 1, c.succ v i z⟫ ∈ s
no goals