no goals
α : Type u_1
s✝ : Heap α
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ Option.map (fun x => x.fst) (deleteMin le (cons r a c s)) = head? le (cons r a c s)
simp only [deleteMin, findMin_val, Option.map, head?]