exact lt_of_inBounds_of_charStep inBounds mem
c : Char
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].charStep c
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
no goals