. assumption
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' ?cons.n t₂

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ ℕ
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ h₂.rank