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