∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} (rank : ℕ)
  (before :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s))
  (node : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank)
  (next : Batteries.BinomialHeap.Imp.Heap.WF le (rank + 1) res.next) (rank_1 : ℕ)
  (before_1 :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank_1 s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s))
  (node_1 : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank_1)
  (next_1 : Batteries.BinomialHeap.Imp.Heap.WF le (rank_1 + 1) res.next),
  ({ rank := rank, before := before, node := node, next := next } =
      { rank := rank_1, before := before_1, node := node_1, next := next_1 }) =
    (rank = rank_1)