[2601] | 1 | open Preamble |
---|

| 2 | |
---|

| 3 | open Hints_declaration |
---|

| 4 | |
---|

| 5 | open Core_notation |
---|

| 6 | |
---|

| 7 | open Pts |
---|

| 8 | |
---|

| 9 | open Logic |
---|

| 10 | |
---|

| 11 | open Types |
---|

| 12 | |
---|

| 13 | open Relations |
---|

| 14 | |
---|

| 15 | open Bool |
---|

| 16 | |
---|

| 17 | type deqSet = |
---|

| 18 | __ -> __ -> Bool.bool |
---|

| 19 | (* singleton inductive, whose constructor was mk_DeqSet *) |
---|

| 20 | |
---|

| 21 | val deqSet_rect_Type4 : |
---|

| 22 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 |
---|

| 23 | |
---|

| 24 | val deqSet_rect_Type5 : |
---|

| 25 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 |
---|

| 26 | |
---|

| 27 | val deqSet_rect_Type3 : |
---|

| 28 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 |
---|

| 29 | |
---|

| 30 | val deqSet_rect_Type2 : |
---|

| 31 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 |
---|

| 32 | |
---|

| 33 | val deqSet_rect_Type1 : |
---|

| 34 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 |
---|

| 35 | |
---|

| 36 | val deqSet_rect_Type0 : |
---|

| 37 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 |
---|

| 38 | |
---|

| 39 | type carr |
---|

| 40 | |
---|

| 41 | val eqb : deqSet -> __ -> __ -> Bool.bool |
---|

| 42 | |
---|

| 43 | val deqSet_inv_rect_Type4 : |
---|

| 44 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 |
---|

| 45 | |
---|

| 46 | val deqSet_inv_rect_Type3 : |
---|

| 47 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 |
---|

| 48 | |
---|

| 49 | val deqSet_inv_rect_Type2 : |
---|

| 50 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 |
---|

| 51 | |
---|

| 52 | val deqSet_inv_rect_Type1 : |
---|

| 53 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 |
---|

| 54 | |
---|

| 55 | val deqSet_inv_rect_Type0 : |
---|

| 56 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 |
---|

| 57 | |
---|

| 58 | val beqb : Bool.bool -> Bool.bool -> Bool.bool |
---|

| 59 | |
---|

| 60 | val deqBool : deqSet |
---|

| 61 | |
---|

| 62 | val eq_option : deqSet -> __ Types.option -> __ Types.option -> Bool.bool |
---|

| 63 | |
---|

| 64 | val deqOption : deqSet -> deqSet |
---|

| 65 | |
---|

| 66 | val eq_pairs : |
---|

| 67 | deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> Bool.bool |
---|

| 68 | |
---|

| 69 | val deqProd : deqSet -> deqSet -> deqSet |
---|

| 70 | |
---|

| 71 | val eq_sum : |
---|

| 72 | deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool |
---|

| 73 | |
---|

| 74 | val deqSum : deqSet -> deqSet -> deqSet |
---|

| 75 | |
---|

| 76 | val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool |
---|

| 77 | |
---|

| 78 | val deqSig : deqSet -> deqSet |
---|

| 79 | |
---|