induction path with
| base _ => exact .base assm
| @step i j k cs cs' step rest ih =>
  have h₂ := step.h₂
  have : start' ≤ j := by
    cases step with
    | charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
    | εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
  exact .step (step.castStart' assm) (ih this)
cs : List Char
nfa : NFA
start start' i i' : ℕ
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
path : nfa.pathIn start i i' cs
⊢ nfa.pathIn start' i i' cs
no goals