induction path with
| base h => exact .base h
| @step i j k cs cs' step _ ih =>
  have eq := eq _ step.h₁ assm
  have : j < nfa.nodes.size := by
    cases step with
    | @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
    | εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
  exact .step (step.cast assm eq.symm) (ih this)
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
path : nfa'.pathIn start i j cs
⊢ nfa.pathIn start i j cs
no goals