+definition zero: \forall (P:COA). P \def
+ \lambda (P:COA). inf P ? (dvoid_ixfam P).
+
+definition one: \forall (P:COA). P \def
+ \lambda (P:COA). sup P ? (dvoid_ixfam P).
+
+definition binf: \forall (P:COA). P \to P \to P \def
+ \lambda (P:COA). \lambda p0,p1.
+ inf P ? (dbool_ixfam P p0 p1).
+
+definition bsup: \forall (P:COA). P \to P \to P \def
+ \lambda (P:COA). \lambda p0,p1.
+ sup P ? (dbool_ixfam P p0 p1).
+