cases e'.rcns_trans_eq_cons e ▸ 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')
⊢ rcn ∉ s₁✝.progress
case head
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress

case tail
α : 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')
a✝ : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress