simp [inBounds] at *
size size' : Nat
n : Node
h : n.inBounds size
le : size ≤ size'
⊢ n.inBounds size'
size size' : Nat
n : Node
h :
  match n with
  | done => True
  | fail => True
  | epsilon next => next < size
  | char c next => next < size
  | split next₁ next₂ => next₁ < size ∧ next₂ < size
  | save offset next => next < size
  | sparse cs next => next < size
le : size ≤ size'
⊢ match n with
  | done => True
  | fail => True
  | epsilon next => next < size'
  | char c next => next < size'
  | split next₁ next₂ => next₁ < size' ∧ next₂ < size'
  | save offset next => next < size'
  | sparse cs next => next < size'