exact .step head (ih h₂)
case step
j i k : ℕ
nfa : NFA
i✝ j✝ k✝ : ℕ
head : j✝ ∈ nfa.εStep i✝
rest✝ : nfa.εClosure j✝ k✝
ih : k ∈ nfa.εClosure k✝ → k ∈ nfa.εClosure j✝
h₂ : k ∈ nfa.εClosure k✝
⊢ k ∈ nfa.εClosure i✝
no goals