obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (∂ (initSeg s)) (s.card - 1)