constructor
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₁ ↔ u ∈ 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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₁ → u ∈ 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 ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
⊢ u ∈ s₂ → u ∈ s₁