case tail h => exact mt e.progress_monotonic (hi h)
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h✝ : rcn ∈ rcns (trans e e')
h : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress
no goals