cases step with
| εStep _ _ step =>
  exact εClosure.step (εStep_of_εStep step) ih
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j []
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
⊢ k ∈ nfa.εClosure i
no goals