subst assm₂
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
h✝ : 0 ≤ j
assm₂ : j = 0
ih : 0 < j → j = 0 → nfa.pathToNext 0 1 j []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
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 ++ [])