no goals
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
h : WF le s
eq : Heap.deleteMin le s = some (a, s')
⊢ WF le s'
cases h with cases eq | node h => exact Heap.WF.combine h
no goals
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c✝ : Heap α
h : NodeWF le a c✝
⊢ WF le (Heap.combine le c✝)
exact Heap.WF.combine h