theory Why2
  use unit_inf.Unit
  use int.Int
  use int.ComputerDivision
  use real.Real
  use bool_inf.Bool
  predicate eq_unit Unit.unit Unit.unit

  predicate neq_unit Unit.unit Unit.unit

  predicate eq_bool Bool.bool Bool.bool

  predicate neq_bool Bool.bool Bool.bool

  predicate lt_int int int

  predicate le_int int int

  predicate gt_int int int

  predicate ge_int int int

  predicate eq_int int int

  predicate neq_int int int

  function add_int int int : int

  function sub_int int int : int

  function mul_int int int : int

  function div_int int int : int

  function mod_int int int : int

  function neg_int int : int

  predicate zwf_zero (a : int) (b : int) = ((Int.(<=) 0 b) /\ (Int.(<) a b))

  goal P_po_1:
    (forall x:int.
      (forall x0:int.
        (forall x1:int.
          ((x0 = (Int.(-) 1 x : int)) ->
           ((x1 = (Int.(-) 1 x0 : int)) -> (x1 = x))))))


end