apply congrArg (λ x => x + 1)
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
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) + 1 = length (y :: ys) + length xs + 1
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
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs