∀ {α : Type u_1} (s₁ : Batteries.BinomialHeap.Imp.Heap α) (r₁ : ℕ) (a₁ : α) (n₁ : Batteries.BinomialHeap.Imp.HeapNode α)
  (t₁ : Batteries.BinomialHeap.Imp.Heap α) (h : 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 α) (h_1 : s₂ = Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂),
  InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun a a_1 => a.length + a_1.length) ⟨s₁, t₂⟩
    ⟨namedPattern s₁ (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁) h,
      namedPattern s₂ (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) h_1⟩