intros
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
⊢ IsBinTree r → y < r.rank → IsHeapForest' r.rank x → IsHeapForest' y (r :: x)
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
a✝² : IsBinTree r
a✝¹ : y < r.rank
a✝ : IsHeapForest' r.rank x
⊢ IsHeapForest' y (r :: x)