. constructor
case h_1
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝² : ℕ
x✝¹ : List (BinTree α✝)
x✝ : ℕ
heq✝ : t :: ts = []
⊢ IsHeapForest' r []

case h_2
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
head✝ : BinTree α✝
as✝ : List (BinTree α✝)
heq✝ : t :: ts = head✝ :: as✝
⊢ IsHeapForest' r as✝

case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
case h_2
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
head✝ : BinTree α✝
as✝ : List (BinTree α✝)
heq✝ : t :: ts = head✝ :: as✝
⊢ IsHeapForest' r as✝

case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)