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

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ ℕ