let FOO = thm `; let P be num->bool; assume !x. P x \/ ~P x; thus (~ ~ ?x. P x) ==> ?x. P x; `;;