unfold Node.charStep at mem
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem : j ∈ node.charStep c
⊢ j < k
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.char c' next => if (c == c') = true then {next} else ∅
    | Node.sparse cs next => if c ∈ cs then {next} else ∅
    | x => ∅
⊢ j < k