Theorem: Regex.NFA.charStep_of_charStep (RegexCorrectness/NFA/Basic.lean)

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