Monotonicity proof rule MR generalizes the postcondition and proves [a]Q instead of [a]P provided that Q is more general so Q→P can be proved. MR is useful when P is another modality [b]R that can be shown from a more general intermediate condition Q.