Theorem: Regex.NFA.εStep_of_εStep (RegexCorrectness/NFA/Basic.lean)

State before:
j : ℕ
nfa : NFA
i : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εStep i
Tactic:
simp [εStep, h, mem]
State after:
no goals