(value :q)
(lp)
(certify-book "dft-ex" 0 nil :defaxioms-okp t)