cases hf
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
h✝² : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) t₁
h : ¬(t₁ = [] ∧ [] = [])
h✝ : ¬hRank t₁ ≤ hRank []
hle : hRank [] ≤ hRank t₁
⊢ h₁.rank + 1 < hRank t₁
case nil
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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
a✝³ : IsBinTree h₁
a✝² : rx < h₁.rank
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) []
h : ¬([] = [] ∧ [] = [])
h✝ : ¬hRank [] ≤ hRank []
hle : hRank [] ≤ hRank []
⊢ h₁.rank + 1 < hRank []

case cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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
a✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² : (h₁.rank + 1 != hRank []) = false
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t✝ :: ts✝)
h : ¬(t✝ :: ts✝ = [] ∧ [] = [])
h✝ : ¬hRank (t✝ :: ts✝) ≤ hRank []
hle : hRank [] ≤ hRank (t✝ :: ts✝)
⊢ h₁.rank + 1 < hRank (t✝ :: ts✝)