have ih₂ : pathToNext nfa' next nfa.nodes.size nfa'.val.start cs₂ := ih₂ eq
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)