RBF Cleanup

This MR includes a set of changes aimed at cleaning up the existing code. Some of the changes include

1. Introduce a new definition total_workload_between to keep it consistent with similar definitions.
2. Remove the duplicate proof for RBF spec (#142 (closed)).

Fixes: #142 (closed)