split at mem <;>
  try simp [Node.inBounds] at * <;>
  try cases mem <;>
  simp [*]
node : Node
j k : ℕ
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.epsilon next => {next}
    | Node.split next₁ next₂ => {next₁, next₂}
    | Node.save offset next => {next}
    | x => ∅
⊢ j < k
no goals