∀ {α : Type u_1} (x : Batteries.BinomialHeap.Imp.HeapNode α),
  x.rank =
    match x with
    | Batteries.BinomialHeap.Imp.HeapNode.nil => 0
    | Batteries.BinomialHeap.Imp.HeapNode.node a child s => s.rank + 1