∀ {α : Type u} {motive : Batteries.PairingHeapImp.Heap α → Sort u_1} (t : Batteries.PairingHeapImp.Heap α)
  (node :
    (a : α) →
      (child sibling : Batteries.PairingHeapImp.Heap α) → motive (Batteries.PairingHeapImp.Heap.node a child sibling))
  («else» : Nat.hasNotBit 2 t.ctorIdx → motive t) (h : Nat.hasNotBit 2 t.ctorIdx),
  Batteries.PairingHeapImp.Heap.combine._sparseCasesOn_1 t node «else» = «else» h