induction ev with
| base h =>
  subst assm₂
  simp
| @step i j k cs cs' step path ih =>
  have ih := ih step.lt_right assm₂
  split
  case inl eqi =>
    subst eqi
    have ⟨ge, node⟩ := rStart_of_spec eq
    simp [node]
    cases step with
    | charStep _ _ step => simp [node, NFA.Node.charStep] at step
    | εStep h₁ h₂ step =>
      apply Or.inr
      have : j = rStart_of eq := by
        simp [node, NFA.Node.εStep] at step
        cases step with
        | inl eq => exact eq
        | inr eq =>
          have : nfa.nodes.size ≤ j := le_of_pathIn_left path
          exact absurd next.isLt (Nat.not_lt_of_le (eq ▸ this))
      subst this
      simp [NFA.Node.εStep]
      have : rStart_of eq ≠ nfa.nodes.size := Nat.ne_of_gt ge
      simp [this] at ih
      exact ih
  case inr nei =>
    have gti : nfa.nodes.size < i := Nat.lt_of_le_of_ne step.h₁ (Ne.symm nei)
    split at ih
    case inl eqj =>
      have toNext : pathToNext result nfa.nodes.size (nfa.nodes.size + 1) i cs :=
        ⟨i, [], cs, rfl, .base gti, (eqj ▸ step).castStart' gti⟩
      cases ih with
      | inl eqs =>
        subst eqs
        exact ⟨cs, [], rfl, toNext, .complete⟩
      | inr cond =>
        obtain ⟨cs₁, cs₂, eqs, path', loop⟩ := cond
        exact ⟨cs, cs₁ ++ cs₂, by simp [eqs], toNext, .loop path' loop⟩
    case inr nej =>
      obtain ⟨cs₁, cs₂, eqs, path', loop⟩ := ih
      subst eqs
      cases step with
      | charStep h₁ h₂ step =>
        exact ⟨_ :: cs₁, cs₂, rfl, path'.cons (.charStep gti h₂ step), loop⟩
      | εStep h₁ h₂ step =>
        exact ⟨cs₁, cs₂, rfl, path'.cons (.εStep gti h₂ step), loop⟩
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
assm₁ : i < (↑result).nodes.size
assm₂ : loopStart = nfa.nodes.size
ev : (↑result).pathIn nfa.nodes.size i loopStart cs
⊢ if i = 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) i cs₁ ∧ starLoop eq cs₂
no goals