simp
case base
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
h : nfa.nodes.size ≤ nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
⊢ if nfa.nodes.size = nfa.nodes.size then
    [] = [] ∨
      ∃ 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₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) nfa.nodes.size cs₁ ∧ starLoop eq cs₂
no goals