intro hc
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
⊢ Execution.Instantaneous.Step.rcn e ≠ i
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
⊢ False