exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
no goals