. constructor <;> assumption
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
no goals