simp [Node.inBounds] at * <;>
try cases mem <;>
simp [*]
case h_4
node : Node
j k : ℕ
inBounds : node.inBounds k
n✝ : Node
x✝² : ∀ (next : ℕ), node = Node.epsilon next → False
x✝¹ : ∀ (next₁ next₂ : ℕ), node = Node.split next₁ next₂ → False
x✝ : ∀ (offset next : ℕ), node = Node.save offset next → False
mem : j ∈ ∅
⊢ j < k
no goals