∀ {α : Type u_1} {lt : α → α → Bool} {n : ℕ}
  (motive : (s : Batteries.BinomialHeap.Imp.Heap α) → Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) s → Prop)
  (s : Batteries.BinomialHeap.Imp.Heap α) (h : Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) s),
  (∀ (h : Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) Batteries.BinomialHeap.Imp.Heap.nil),
      motive Batteries.BinomialHeap.Imp.Heap.nil h) →
    (∀ (rank : ℕ) (val : α) (node : Batteries.BinomialHeap.Imp.HeapNode α) (next : Batteries.BinomialHeap.Imp.Heap α)
        (h : Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) (Batteries.BinomialHeap.Imp.Heap.cons rank val node next)),
        motive (Batteries.BinomialHeap.Imp.Heap.cons rank val node next) h) →
      motive s h