split <;> apply IsSearchTree_findMin <;> assumption
case cons
α : 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
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsSearchTree le h'
a✝¹ : IsSearchTree le h
a✝ : IsMinHeap le (Heap.heap hs)
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
no goals