∀ {α : Type u_1} {sz : ℕ} (lt : α → α → Bool) (_x : (_ : Vector α sz) ×' Fin sz),
  Batteries.BinaryHeap.heapifyUp._unary lt _x =
    PSigma.casesOn _x fun a i =>
      match i with
      | ⟨0, isLt⟩ => a
      | ⟨i'.succ, hi⟩ =>
        let j := i' / 2;
        if lt a[j] a[i] = true then Batteries.BinaryHeap.heapifyUp._unary lt ⟨a.swap (↑i) j ⋯ ⋯, ⟨j, ⋯⟩⟩ else a