. rfl
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 h
ht₂ : IsHeapForest' r []
h✝ : hRank h ≤ hRank []
⊢ hRank h ≤ hRank 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 h
ht₂ : IsHeapForest' r []
h✝ : ¬hRank h ≤ hRank []
⊢ hRank [] ≤ hRank 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 h
ht₂ : IsHeapForest' r []
h✝ : ¬hRank h ≤ hRank []
⊢ hRank [] ≤ hRank h