(*
    Example proof script for PhoX Proof General

    example.phx,v 9.0 2008/01/30 15:22:21 da Exp
*)

(*
goal /\n:N (ack n N1 >= N2).
intro 2.
elim H.
trivial.
elim -1 [case] H0.
trivial.
trivial.
save ack_lem7.
*)

prop (* test *) (* just un test *) test /\X (X -> X).
print $0.
trivial.
save.