contradiction
α : 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
this✝ : Nodup (rcns (trans e e'))
this : ¬Nodup (Execution.Instantaneous.Step.rcn e :: rcns e')
⊢ False
no goals