assumption
case cons.a
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝³ : IsBinTree t✝
a✝² : IsHeapForest' t✝.rank ts✝
a✝¹ : rx < t✝.rank
a✝ : ry < hRank (t✝ :: ts✝)
⊢ IsHeapForest' t✝.rank ts✝
no goals