induction path with
| base h => exact .base (Nat.le_trans le h)
| step step _ ih => exact .step (step.castStart le) ih
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ start
path : nfa.pathIn start i j cs
⊢ nfa.pathIn start' i j cs
no goals