. have he₁ := h.left
  have he₂ := h.right
  simp[he₁, he₂]
  constructor
case pos
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : t₁ = [] ∧ t₂ = []
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)

case neg
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
case neg
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)