This MR implements #91 (closed): it generalizes the proofmode to arbitrary BIs.
This will create a new commit in order to revert the existing changes.
