1 FOLP = IFOLP +
2 consts
3 cla :: "[p=>p]=>p"
4 rules
5 classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P"
6 end