simp[split]
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a : α
⊢ let spl := split [x, y, a];
  List.length spl.fst < List.length [a] + 2 ∧ List.length spl.snd < List.length [a] + 2
no goals