have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
          length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)