:load Bool.cloe

Eq_Equal
 (X:*)
 = X -> X -> Bool

Eq_Class
 (X:*) (Data:*)
 = (equal:Eq_Equal X)
 -> Data
Eq_Polytype
 (X:*) : *p
 = (Data:*) -> Eq_Class X Data -> Data
Eq
 (X:*) : *m
 = Monotype (Eq_Polytype X)

eq
 (X:*)
 (equal:Eq_Equal X)
 : Eq X
 = monotype (Eq_Polytype X)
     (λ(Data:*) (eq_class:Eq_Class X Data) -> eq_class equal)
unEq
 (X:*) (Data:*)
 (eq_class:Eq_Class X Data)
 (eq:Eq X)
 : Data
 = polytype (Eq_Polytype X) eq Data eq_class

Eq_equal
 (X:*) (eq:Eq X)
 : Eq_Equal X
 = unEq X (Eq_Equal X)
    (λ(equal:Eq_Equal X) -> equal)
    eq