case neg =>
  constructor <;> intro hm
  case' mp  => have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
  case' mpr => have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
  all_goals exact (Set.mem_union ..).mp h |>.resolve_left hc
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
no goals