cases e
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : Tail s₁ s₂
⊢ s₁ = s₂
case none
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁

case some
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
a✝ : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂