module Choice

  (* no why3 type is empty. *)

  constant default : 'a

  (* Axiom of choice : we can explicitely pick an element whom
     existence is proven. *)

  function choice (p: 'a -> bool) : 'a
  axiom choice_behaviour : forall p: 'a -> bool, x: 'a.
    p x -> p (choice p)

end