rw [hr₁, hr₂] at *
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress