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)
cs✝ : List Char
nfa : NFA
start start' i✝ 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
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ start' ≤ j
no goals