apply IsHeapForest'_weaken hxs
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ IsHeapForest' (min rx ry) h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ min rx ry ≤ rx