(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)
        )))