no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
h : split (a :: b :: l) = (l₁, l₂)
⊢ mergeSort r (a :: b :: l) = merge r (mergeSort r l₁) (mergeSort r l₂)
simp only [mergeSort, h]