induction h with
| base => exact .base (Nat.zero_le _)
| @step i j k step _ ih =>
  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
i i' : ℕ
nfa : NFA
h : i' ∈ nfa.εClosure i
⊢ nfa.pathIn 0 i i' []
no goals