apply pushRegex.alternate eq
case alternate
i j : ℕ
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
i j : ℕ
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ ∀ (nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa').nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → j = ↑next ∨ nfa.nodes.size ≤ j