examples/logic/First.why

   1 theory First
   2
   3   type t
   4   constant c : t
   5   predicate a
   6   predicate p t
   7   predicate q t
   8   function f (t) : t
   9
  10   goal P1 : (forall x:t. p(x)) -> (exists x:t. p(x))
  11   goal P5 : (forall x:t. p(x) -> p(f(x))) -> forall x:t.p(x) -> p(f(f(x)))
  12
  13 end