rename_i hneq
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
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✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
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✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)