cases Nat.decLt i nfa.nodes.size with
| isTrue lt =>
  simp [εStep, lt] at step
  exact .step (.εStep (Nat.zero_le _) lt step) ih
| isFalse nlt => simp [εStep, nlt] at step
case mpr.step
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
⊢ nfa.pathIn 0 i k []
no goals