simp [e.progress_eq, Set.ssubset_iff_insert]
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ s₁.progress ⊂ s₂.progress
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ ∃ a ∉ s₁.progress, insert a s₁.progress ⊆ Set.insert (rcn e) s₁.progress