induction e <;> try cases ‹_ ↓ _›
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
n : State.Nontrivial s₁
e : s₁ ⇓ s₂
⊢ Nonempty (Grouped s₁ s₂)
case refl
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
⊢ Nonempty (Grouped s✝ s✝)

case trans.skip
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.exec
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.time
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)