apply Iff.intro
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] ↔ i' ∈ nfa.εClosure i
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i

case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []