∀ {α : Type u_1} (le : α → α → Bool) (k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α)
  (x : Batteries.BinomialHeap.Imp.Heap α) (x_1 : Batteries.BinomialHeap.Imp.FindMin α),
  Batteries.BinomialHeap.Imp.Heap.findMin le k x x_1 =
    match x, x_1 with
    | Batteries.BinomialHeap.Imp.Heap.nil, res => res
    | Batteries.BinomialHeap.Imp.Heap.cons r a c s, res =>
      Batteries.BinomialHeap.Imp.Heap.findMin le (k ∘ Batteries.BinomialHeap.Imp.Heap.cons r a c) s
        (if le res.val a = true then res else { before := k, val := a, node := c, next := s })