∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool}
  {k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α}
  {res : Batteries.BinomialHeap.Imp.FindMin α},
  (Batteries.BinomialHeap.Imp.Heap.findMin le k s res).val = Batteries.BinomialHeap.Imp.Heap.headD le res.val s