constructor
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x : M
⊢ x ∈ u ↔ ∃ y, ⟪x, y⟫ ∈ s
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x : M
⊢ x ∈ u → ∃ y, ⟪x, y⟫ ∈ s

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ y < s, ∃ z ∈ s, z = ⟪x, y⟫
x : M
⊢ (∃ y, ⟪x, y⟫ ∈ s) → x ∈ u