let prove_example1() =
  begin
    printf "\nprove_example1\n";

    let ctx        = mk_context [||] in
    
    (* create uninterpreted type. *)
    let u_name     = Z3.mk_string_symbol ctx "U" in
    let u          = Z3.mk_uninterpreted_sort ctx u_name in
    
    (* declare function g *)
    let g_name      = Z3.mk_string_symbol ctx "g" in
    let g           = Z3.mk_func_decl ctx g_name [|u|] u in

    (* create x and y *)
    let x_name      = Z3.mk_string_symbol ctx "x" in
    let y_name      = Z3.mk_string_symbol ctx "y" in
    let x           = Z3.mk_const ctx x_name u in
    let y           = Z3.mk_const ctx y_name u in
    (* create g(x), g(y) *)
    let gx          = mk_unary_app ctx g x in
    let gy          = mk_unary_app ctx g y in
    
    (* assert x = y *)
    let eq          = Z3.mk_eq ctx x y in
    Z3.assert_cnstr ctx eq;

    (* prove g(x) = g(y) *)
    let f           = Z3.mk_eq ctx gx gy in
    printf "prove: x = y implies g(x) = g(y)\n";
    prove ctx f true;

    (* create g(g(x)) *)
    let ggx         = mk_unary_app ctx g gx in
    
    (* disprove g(g(x)) = g(y) *)
    let f           = Z3.mk_eq ctx ggx gy in
    printf "disprove: x = y implies g(g(x)) = g(y)\n";
    prove ctx f false;

    Z3.del_context ctx;
  end