simp [e.unprocessed_eq, Set.ssubset_iff_subset_ne]
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ unprocessed s₂ ⊂ unprocessed s₁
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ rcn e ∈ unprocessed s₁