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

| 2 | |
---|

| 3 | open Hints_declaration |
---|

| 4 | |
---|

| 5 | open Core_notation |
---|

| 6 | |
---|

| 7 | open Pts |
---|

| 8 | |
---|

| 9 | open Logic |
---|

| 10 | |
---|

| 11 | type sigma = |
---|

| 12 | __ |
---|

| 13 | (* singleton inductive, whose constructor was mk_Sigma *) |
---|

| 14 | |
---|

| 15 | val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1 |
---|

| 16 | |
---|

| 17 | val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 |
---|

| 18 | |
---|

| 19 | val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 |
---|

| 20 | |
---|

| 21 | val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 |
---|

| 22 | |
---|

| 23 | val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 |
---|

| 24 | |
---|

| 25 | val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 |
---|

| 26 | |
---|

| 27 | val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 |
---|

| 28 | |
---|

| 29 | val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 |
---|

| 30 | |
---|

| 31 | val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 |
---|

| 32 | |
---|

| 33 | val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 |
---|

| 34 | |
---|

| 35 | val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 |
---|

| 36 | |
---|

| 37 | type p1 = __ |
---|

| 38 | |
---|

| 39 | val p2 : sigma -> p1 |
---|

| 40 | |
---|

| 41 | val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 |
---|

| 42 | |
---|

| 43 | val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 |
---|

| 44 | |
---|

| 45 | val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 |
---|

| 46 | |
---|

| 47 | val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 |
---|

| 48 | |
---|

| 49 | val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 |
---|

| 50 | |
---|

| 51 | val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 |
---|

| 52 | |
---|

| 53 | val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 |
---|

| 54 | |
---|

| 55 | val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 |
---|

| 56 | |
---|

| 57 | val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 |
---|

| 58 | |
---|

| 59 | val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 |
---|

| 60 | |
---|

| 61 | val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 |
---|

| 62 | |
---|

| 63 | val jmeq_discr : 'a1 -> 'a2 -> __ |
---|

| 64 | |
---|

| 65 | val cast : 'a1 -> 'a2 |
---|

| 66 | |
---|

| 67 | type ('a, 'x) curry = 'x |
---|

| 68 | |
---|

| 69 | val g : 'a1 -> 'a2 -> 'a1 -> 'a2 |
---|

| 70 | |
---|

| 71 | type 'p pP = 'p |
---|

| 72 | |
---|

| 73 | val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP |
---|

| 74 | |
---|

| 75 | val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 |
---|

| 76 | |
---|