simp [*]
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches [c] (Expr.char c)