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