cases mem
case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
case h_2.intro
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
left✝ : c ∈ cs✝
right✝ : j = next✝
⊢ j < k