∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Sort u_2) (a : α) (c s : Batteries.PairingHeapImp.Heap α)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil)
  (h_2 : (a : α) → (c s : Batteries.PairingHeapImp.Heap α) → motive (Batteries.PairingHeapImp.Heap.node a c s)),
  (match Batteries.PairingHeapImp.Heap.node a c s with
    | Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.node a c s => h_2 a c s) =
    h_2 a c s