have eq := eq _ step.h₁ assm
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 cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
⊢ nfa.pathIn start i k (cs ++ cs')
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 cs' : List Char
step : nfa'.stepIn start i j cs
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]
⊢ nfa.pathIn start i k (cs ++ cs')