exact ⟨cs, cs', rfl, pathToNext, rest⟩
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size i cs
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
no goals