induction path with
| base h =>
  exact .step (.εStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
| step step' rest ih =>
  have ih := ih assm step
  exact .step (step'.castStart (Nat.min_le_left _ _)) ih
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start : ℕ
assm : j < nfa.nodes.size
step : k ∈ nfa[j].εStep
path : nfa.pathIn start i j cs
⊢ nfa.pathIn (min start k) i k cs
no goals