. intro h
  induction h with
  | base => exact .base (Nat.zero_le _)
  | @step i j k step _ ih =>
    cases Nat.decLt i nfa.nodes.size with
    | isTrue lt =>
      simp [εStep, lt] at step
      exact .step (.εStep (Nat.zero_le _) lt step) ih
    | isFalse nlt => simp [εStep, nlt] at step
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
no goals