∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (h : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.Heap.nil h)
  (h_2 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive h Batteries.BinomialHeap.Imp.Heap.nil)
  (h_3 :
    (s₁ : Batteries.BinomialHeap.Imp.Heap α) →
      (r₁ : ℕ) →
        (a₁ : α) →
          (n₁ : Batteries.BinomialHeap.Imp.HeapNode α) →
            (t₁ : Batteries.BinomialHeap.Imp.Heap α) →
              s₁ = Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁ →
                (s₂ : Batteries.BinomialHeap.Imp.Heap α) →
                  (r₂ : ℕ) →
                    (a₂ : α) →
                      (n₂ : Batteries.BinomialHeap.Imp.HeapNode α) →
                        (t₂ : Batteries.BinomialHeap.Imp.Heap α) →
                          s₂ = Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂ →
                            motive (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁)
                              (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂)),
  (h = Batteries.BinomialHeap.Imp.Heap.nil → False) →
    (match h, Batteries.BinomialHeap.Imp.Heap.nil with
      | Batteries.BinomialHeap.Imp.Heap.nil, h => h_1 h
      | h, Batteries.BinomialHeap.Imp.Heap.nil => h_2 h
      | s₁@h:(Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁),
        s₂@h_4:(Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) => h_3 s₁ r₁ a₁ n₁ t₁ h s₂ r₂ a₂ n₂ t₂ h_4) =
      h_2 h