∀ {α : Type u_1} {le : α → α → Bool} {a : α} {res : Batteries.BinomialHeap.Imp.Heap α}
  (motive :
    (x : ℕ) →
      (x_1 : Batteries.BinomialHeap.Imp.HeapNode α) →
        Batteries.BinomialHeap.Imp.HeapNode.WF le a x_1 x → Batteries.BinomialHeap.Imp.Heap.WF le x_1.rank res → Prop)
  (x : ℕ) (x_1 : Batteries.BinomialHeap.Imp.HeapNode α) (x_2 : Batteries.BinomialHeap.Imp.HeapNode.WF le a x_1 x)
  (x_3 : Batteries.BinomialHeap.Imp.Heap.WF le x_1.rank res),
  (∀ (x : ℕ) (x_4 : Batteries.BinomialHeap.Imp.HeapNode.WF le a Batteries.BinomialHeap.Imp.HeapNode.nil x)
      (hr : Batteries.BinomialHeap.Imp.Heap.WF le Batteries.BinomialHeap.Imp.HeapNode.nil.rank res),
      motive x Batteries.BinomialHeap.Imp.HeapNode.nil x_4 hr) →
    (∀ (a_1 : α) (c s : Batteries.BinomialHeap.Imp.HeapNode α) (n : ℕ)
        (left : ∀ [Batteries.TotalBLE le], le a a_1 = true) (h : Batteries.BinomialHeap.Imp.HeapNode.WF le a_1 c n)
        (h' : Batteries.BinomialHeap.Imp.HeapNode.WF le a s n)
        (hr : Batteries.BinomialHeap.Imp.Heap.WF le (Batteries.BinomialHeap.Imp.HeapNode.node a_1 c s).rank res),
        motive (n + 1) (Batteries.BinomialHeap.Imp.HeapNode.node a_1 c s) ⋯ hr) →
      motive x x_1 x_2 x_3