Gödel Vacuous rule GV proves [a]P by proving ∀xP after universally quantifying over all variables x changed by a. This is helpful when P is mostly independent of a.