exact .step (step.castStart' assm) (ih this)
case step
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
this : start' ≤ j
⊢ nfa.pathIn start' i k (cs ++ cs')
no goals