apply pushRegex.group eq
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = 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
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = 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
⊢ ∀ (nfa'_1 : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa' // (↑nfa'_1).nodes.size < nfa'.nodes.size })
    (nfa''' : { nfa' // (↑nfa'').nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa'_1 = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds' →
      nfa'' = (↑nfa'_1).pushRegex (↑nfa'_1).start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds''' →
          nfa' = ⟨↑nfa''', property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs