all_goals
  case _ hi e =>
    let ⟨steps, tail⟩ := hi $ e.preserves_nontrivial n
    exact match steps, tail with
    | .refl,                   .none    => ⟨.refl, .some $ .single e⟩ 
    | .refl,                   .some e' => ⟨.refl, .some $ .trans e e'⟩
    | .step (.inst ⟨f, h⟩) f', tl       => ⟨.step (.inst ⟨.trans e f, h⟩) f', tl⟩
    | .step (.time f) f',      tl       => ⟨.step (.inst ⟨.single e, f.closed⟩) $ .step f f', tl⟩
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₃✝)
no goals