+
+nlemma bool_is_comparable : comparable.
+ @ bool
+ ##[ napply false
+ ##| napply forall_bool
+ ##| napply eq_bool
+ ##| napply eqbool_to_eq
+ ##| napply eq_to_eqbool
+ ##| napply neqbool_to_neq
+ ##| napply neq_to_neqbool
+ ##| napply decidable_bool
+ ##| napply symmetric_eqbool
+ ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr bool_is_comparable ≡ bool.