simp [Partial.mem_def, e.progress_def ▸ e.exec.mem_rcns_iff (rcn := rcn)]
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ| s₂
⊢ rcn ∈ rcns e ↔ rcn ∈ s₁.rtr[Component.rcn] ∧ rcn ∉ s₁.progress
no goals