Proof:
qed
The derived inference rule BfGen can also be referred to as Gen (analogous to the inference rule BoxGen).