(insert into metaprl/theories/itt/core/itt_logic.ml:
let f1 = << all x:'T. 'p['x] and exst y:'T. 'q['y] => exst z:'T. ('p['z] or not{'q['z]}) >>
let f2 = << exst x:'T. 'a['x] and exst y:'T. 'b['y] => all z:'T. (not{'a['z]} or 'b['z]) >>
and insert into  metaprl/theories/itt/core/itt_logic.mli:
topval f1 : term
topval f2 : term

compile:)

traths@jk-002 ~/metaprl$ omake
*** omake: reading OMakefiles
*** omake: finished reading OMakefiles (0.6 sec)
*** omake: done (64.9 sec, 3/4075 scans, 3/4075 rules, 8/7081 digests)

(start MetaPRL-Editor in new terminal:)

[traths@jk-002 ~/metaprl]$ ./editor/ml/mpxterm &
[2] 2263
[traths@jk-002 ~/metaprl]$

MetaPRL 0.9.6.4+:
        build [Wed Dec 21 19:55:21 2005]
        on jk-002.soft.cs.uni-potsdam.de
        Uses VERBOSE Refiner_ds

# cd "itt_logic";;
Module: /itt_logic
/itt_logic : string
# f1;;          (* show formula *)
  ...
# prove f1;;    (* prove formula *)
0 ms
() : unit
# f2;;
  ...
# prove f2;;
Uncaught exception: Refine error:
                        Jprover: formula is not provable
# exit ();;
MetaPRL exiting

[traths@jk-005 ~/metaprl]$