Computer Science at its most beautiful: ForAll = λP.(P=λx.T)