∀ {α : Type u_1}
  (motive :
    (s : Batteries.PairingHeapImp.Heap α) →
      (∀ (a : α) (child : Batteries.PairingHeapImp.Heap α) (a_1 : α) (child_1 s_1 : Batteries.PairingHeapImp.Heap α),
          s = Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s_1) → False) →
        Prop)
  (s : Batteries.PairingHeapImp.Heap α)
  (x :
    ∀ (a : α) (child : Batteries.PairingHeapImp.Heap α) (a_1 : α) (child_1 s_1 : Batteries.PairingHeapImp.Heap α),
      s = Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s_1) → False),
  (∀
      (x :
        ∀ (a : α) (child : Batteries.PairingHeapImp.Heap α) (a_1 : α) (child_1 s : Batteries.PairingHeapImp.Heap α),
          Batteries.PairingHeapImp.Heap.nil =
              Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) →
            False),
      motive Batteries.PairingHeapImp.Heap.nil x) →
    (∀ (a : α) (child : Batteries.PairingHeapImp.Heap α)
        (x :
          ∀ (a_1 : α) (child_1 : Batteries.PairingHeapImp.Heap α) (a_2 : α)
            (child_2 s : Batteries.PairingHeapImp.Heap α),
            Batteries.PairingHeapImp.Heap.node a child Batteries.PairingHeapImp.Heap.nil =
                Batteries.PairingHeapImp.Heap.node a_1 child_1 (Batteries.PairingHeapImp.Heap.node a_2 child_2 s) →
              False),
        motive (Batteries.PairingHeapImp.Heap.node a child Batteries.PairingHeapImp.Heap.nil) x) →
      (∀ (a : α) (child : Batteries.PairingHeapImp.Heap α) (a_1 : α) (child_1 s : Batteries.PairingHeapImp.Heap α)
          (x :
            ∀ (a_2 : α) (child_2 : Batteries.PairingHeapImp.Heap α) (a_3 : α)
              (child_3 s_1 : Batteries.PairingHeapImp.Heap α),
              Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) =
                  Batteries.PairingHeapImp.Heap.node a_2 child_2 (Batteries.PairingHeapImp.Heap.node a_3 child_3 s_1) →
                False),
          motive (Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s)) x) →
        motive s x