split <;> simp at h <;> try simp
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'
case h_3
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'