refactor: implement `BinaryHeap` using `Vector`

[fgdorais]

This is a follow-up to #849 which uses #793 to simplify major parts of the code, paving the way toward correctness proofs for BinaryHeap.

• [x] Depends on #849
• [x] Depends on #793