split
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
⊢ (if hRank [] ≤ hRank h then hRank [] else hRank h) ≤ hRank (mergeNodes le [] h)
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : hRank [] ≤ hRank h
⊢ hRank [] ≤ hRank (mergeNodes le [] h)

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : ¬hRank [] ≤ hRank h
⊢ hRank h ≤ hRank (mergeNodes le [] h)