| false : bool.
(* operatori booleani *)
-
ndefinition eq_bool ≝
λb1,b2:bool.match b1 with
[ true ⇒ match b2 with [ true ⇒ true | false ⇒ false ]
for @{ 'xor_bool $a $b }.
interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
+(* iteratore sugli esadecimali *)
+ndefinition forall_bool ≝ λP.P true ⊗ P false.
+
ndefinition boolRelation : Type → Type ≝
λA:Type.A → A → bool.