simp [hi $ e.progress_monotonic h]
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn e ∨ rcn ∈ rcns e')
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn e