have ih := ih this assm₂
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih✝ : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
ih : nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))