simp [Node.inBounds] at *
case h_3
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
n✝ : Node
x✝¹ : ∀ (c' : Char) (next : ℕ), node = Node.char c' next → False
x✝ : ∀ (cs : Data.Classes) (next : ℕ), node = Node.sparse cs next → False
mem : j ∈ ∅
⊢ j < k
no goals