(def-atomic-sort boole
*"lambda(n:zz, n = [-1] or n = 1)"*
(theory h-o-real-arithmetic))

(def-constant true%val
*"1"*
(sort *"boole"*)
(theory h-o-real-arithmetic))

(def-constant false%val
*"[-1]"*
(sort *"boole"*)
(theory h-o-real-arithmetic))

(def-constant is%true
*"lambda(b:boole, b = true%val)"*
(theory h-o-real-arithmetic))

(def-constant is%false
*"lambda(b:boole, b = false%val)"*
(theory h-o-real-arithmetic))

(def-theorem true%val-is-true
*"is%true(true%val) iff truth"*
(usages rewrite)
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally is%true)
)))

(def-theorem false%val-is-not-true
*"is%true(false%val) iff falsehood"*
(usages rewrite)
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally is%true)
unfold-defined-constants
)))

(def-theorem true%val-is-not-false
*"is%false(true%val) iff falsehood"*
(usages rewrite)
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally is%false)
unfold-defined-constants
)))

(def-theorem false%val-is-false
*"is%false(false%val) iff truth"*
(usages rewrite)
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally is%false)
)))