exact pathToNext_of_matches.concat eq ih₁ ih₂
case concat
r : Data.Expr
cs cs₁ cs₂ : List Char
r₁ r₂ : Data.Expr
a✝¹ : Data.Expr.matches cs₁ r₁
a✝ : Data.Expr.matches cs₂ r₂
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₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
no goals