intro t ⟨ht, Ht⟩
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
⊢ ∀ (y : M), (y < exp a ∧ ∀ i < a, i ∈ y ↔ P i) → y = s
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
⊢ t = s