∀ {α : Type u_1} {le : α → α → Bool} {a : α}
  (motive : (s : Batteries.PairingHeapImp.Heap α) → Batteries.PairingHeapImp.Heap.NodeWF le a s → Prop)
  (s : Batteries.PairingHeapImp.Heap α) (h : Batteries.PairingHeapImp.Heap.NodeWF le a s),
  (∀ (h : Batteries.PairingHeapImp.Heap.NodeWF le a Batteries.PairingHeapImp.Heap.nil),
      motive Batteries.PairingHeapImp.Heap.nil h) →
    (∀ (_b : α) (_c : Batteries.PairingHeapImp.Heap α)
        (h :
          Batteries.PairingHeapImp.Heap.NodeWF le a
            (Batteries.PairingHeapImp.Heap.node _b _c Batteries.PairingHeapImp.Heap.nil)),
        motive (Batteries.PairingHeapImp.Heap.node _b _c Batteries.PairingHeapImp.Heap.nil) h) →
      (∀ (_b₁ : α) (_c₁ : Batteries.PairingHeapImp.Heap α) (_b₂ : α) (_c₂ _s : Batteries.PairingHeapImp.Heap α)
          (h :
            Batteries.PairingHeapImp.Heap.NodeWF le a
              (Batteries.PairingHeapImp.Heap.node _b₁ _c₁ (Batteries.PairingHeapImp.Heap.node _b₂ _c₂ _s))),
          motive (Batteries.PairingHeapImp.Heap.node _b₁ _c₁ (Batteries.PairingHeapImp.Heap.node _b₂ _c₂ _s)) h) →
        motive s h