simp [e.progress_eq, or_and_right]
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e ↔ rcn ∈ s₂.progress ∧ rcn ∉ s₁.progress
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e → rcn ∉ s₁.progress