Universal Quantification by Case Analysis