exact ih
case εStep.h
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i loopStart : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
k : ℕ
cs' : List Char
assm₂ : k = nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
path : (↑result).pathIn nfa.nodes.size (rStart_of eq) k cs'
ih✝ :
  rStart_of eq < (↑result).nodes.size →
    k = nfa.nodes.size →
      if rStart_of eq = nfa.nodes.size then
        cs' = [] ∨
          ∃ cs₁ cs₂,
            cs' = cs₁ ++ cs₂ ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
      else
        ∃ cs₁ cs₂,
          cs' = cs₁ ++ cs₂ ∧
            (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
step : rStart_of eq ∈ (↑result)[nfa.nodes.size].εStep
this : rStart_of eq ≠ nfa.nodes.size
ih :
  ∃ cs₁ cs₂,
    cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂,
    cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
no goals