assumption
case cons.a
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
m : ℕ
hle : m ≤ n
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝¹ : IsBinTree t✝
a✝ : IsHeapForest' t✝.rank ts✝
hlt : n < t✝.rank
⊢ IsHeapForest' t✝.rank ts✝
no goals