simp_all [Closed, ←Partial.Nonempty.iff_ids_nonempty]
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : Closed s
⊢ Set.Nonempty s.progress
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : s.progress = Partial.ids (s.rtr[Component.rcn])
⊢ Partial.Nonempty (s.rtr[Component.rcn])