exact match hi $ e.preserves_nontrivial n with
| ⟨.refl, tl⟩              => ⟨.step e .refl, tl⟩ 
| ⟨.step (.inst f) f', tl⟩ => ⟨.step (.time e) $ .step f f', tl⟩
| ⟨.step (.time f) _, _⟩   => e.nonrepeatable f n |>.elim
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
no goals