simp
case intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
val✝ : Fintype α
hr : r > 0
h₁ : IsInitSeg ∅ r
⊢ IsInitSeg (∂ ∅) (r - 1)
no goals