+(*
+In this Chapter we shall develop a naif theory of sets represented as
+characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type
+A→Prop.
+For instance the empty set is defined by the always false function: *)