19 (* singleton inductive, whose constructor was mk_DeqSet *)
21 val deqSet_rect_Type4 :
22 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
24 val deqSet_rect_Type5 :
25 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
27 val deqSet_rect_Type3 :
28 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
30 val deqSet_rect_Type2 :
31 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
33 val deqSet_rect_Type1 :
34 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
36 val deqSet_rect_Type0 :
37 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
41 val eqb : deqSet -> __ -> __ -> Bool.bool
43 val deqSet_inv_rect_Type4 :
44 deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
46 val deqSet_inv_rect_Type3 :
47 deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
49 val deqSet_inv_rect_Type2 :
50 deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
52 val deqSet_inv_rect_Type1 :
53 deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
55 val deqSet_inv_rect_Type0 :
56 deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
58 val beqb : Bool.bool -> Bool.bool -> Bool.bool
62 val eq_option : deqSet -> __ Types.option -> __ Types.option -> Bool.bool
64 val deqOption : deqSet -> deqSet
67 deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> Bool.bool
69 val deqProd : deqSet -> deqSet -> deqSet
72 deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool
74 val deqSum : deqSet -> deqSet -> deqSet
76 val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool
78 val deqSig : deqSet -> deqSet