cases e
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ w✝
⊢ ¬rcn <[rtr] rcn
case skip
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
s✝ : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn

case exec
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e✝ : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn

case time
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
t✝ : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn