exact .step (.εStep (Nat.zero_le _) lt step) ih
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathIn 0 i k []
no goals