intro _
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e