{α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.Heap α) →
      (x_1 : Batteries.BinomialHeap.Imp.FindMin α) →
        ((res : Batteries.BinomialHeap.Imp.FindMin α) → motive Batteries.BinomialHeap.Imp.Heap.nil res) →
          ((r : ℕ) →
              (a : α) →
                (c : Batteries.BinomialHeap.Imp.HeapNode α) →
                  (s : Batteries.BinomialHeap.Imp.Heap α) →
                    (res : Batteries.BinomialHeap.Imp.FindMin α) →
                      motive (Batteries.BinomialHeap.Imp.Heap.cons r a c s) res) →
            motive x x_1