exact le_of_pathIn_left path
case intro.intro.intro.intro.intro
nfa : NFA
next i : ℕ
cs : List Char
start w✝² : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : nfa.pathIn start i w✝² w✝¹
right✝ : nfa.stepIn start w✝² next w✝
⊢ start ≤ i
no goals