induction path with
| base h => exact .base h
| step step _ ih =>
  let ⟨h, eq⟩ := eq _ step.h₁ step.h₂
  exact .step (step.cast h eq) ih
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
path : nfa.pathIn start i j cs
⊢ nfa'.pathIn start i j cs
no goals