simp[findMin]
α : Type u_1
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 : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsHeapForest' r (h :: hs)
hh' : IsBinTree h'
⊢ IsBinTree (findMin le (h :: hs) idx (h', idx')).fst
α : Type u_1
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 : ℕ
h : BinTree α
hs : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsHeapForest' r (h :: hs)
hh' : IsBinTree h'
⊢ IsBinTree
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst