exact lt_of_εStep (eq.symm ▸ step)
case εStep
i✝ j✝ : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs' : List Char
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
h₁✝ : start ≤ i
h₂✝ : i < nfa'.nodes.size
step : j ∈ nfa'[i].εStep
⊢ j < nfa.nodes.size
no goals