apply Set.insert_union'
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ Set.insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress ∪ {a | a ∈ rcns a✝} =
    s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
no goals