. contradiction
case inr.inr.inr.inl.a.inr.inl.cons.nil
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' r []
ih : min (hRank []) (h₁.rank + 1) ≤ hRank (mergeNodes le [] (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank []) = false
h✝ : hRank [] ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank []

case inr.inr.inr.inl.a.inr.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)
case inr.inr.inr.inl.a.inr.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)