ext i
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ unprocessed s₂ = unprocessed s₁ \ {rcn e}
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}