[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 | let rec sigma_rect_Type4 h_mk_Sigma x_890 = |
---|
| 17 | let x_891 = x_890 in h_mk_Sigma __ x_891 |
---|
| 18 | |
---|
| 19 | (** val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 **) |
---|
| 20 | let rec sigma_rect_Type5 h_mk_Sigma x_893 = |
---|
| 21 | let x_894 = x_893 in h_mk_Sigma __ x_894 |
---|
| 22 | |
---|
| 23 | (** val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 **) |
---|
| 24 | let rec sigma_rect_Type3 h_mk_Sigma x_896 = |
---|
| 25 | let x_897 = x_896 in h_mk_Sigma __ x_897 |
---|
| 26 | |
---|
| 27 | (** val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 **) |
---|
| 28 | let rec sigma_rect_Type2 h_mk_Sigma x_899 = |
---|
| 29 | let x_900 = x_899 in h_mk_Sigma __ x_900 |
---|
| 30 | |
---|
| 31 | (** val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 **) |
---|
| 32 | let rec sigma_rect_Type1 h_mk_Sigma x_902 = |
---|
| 33 | let x_903 = x_902 in h_mk_Sigma __ x_903 |
---|
| 34 | |
---|
| 35 | (** val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 **) |
---|
| 36 | let rec sigma_rect_Type0 h_mk_Sigma x_905 = |
---|
| 37 | let x_906 = x_905 in h_mk_Sigma __ x_906 |
---|
| 38 | |
---|
| 39 | (** val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 40 | let sigma_inv_rect_Type4 hterm h1 = |
---|
| 41 | let hcut = sigma_rect_Type4 h1 hterm in hcut __ |
---|
| 42 | |
---|
| 43 | (** val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 44 | let sigma_inv_rect_Type3 hterm h1 = |
---|
| 45 | let hcut = sigma_rect_Type3 h1 hterm in hcut __ |
---|
| 46 | |
---|
| 47 | (** val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 48 | let sigma_inv_rect_Type2 hterm h1 = |
---|
| 49 | let hcut = sigma_rect_Type2 h1 hterm in hcut __ |
---|
| 50 | |
---|
| 51 | (** val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 52 | let sigma_inv_rect_Type1 hterm h1 = |
---|
| 53 | let hcut = sigma_rect_Type1 h1 hterm in hcut __ |
---|
| 54 | |
---|
| 55 | (** val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 56 | let sigma_inv_rect_Type0 hterm h1 = |
---|
| 57 | let hcut = sigma_rect_Type0 h1 hterm in hcut __ |
---|
| 58 | |
---|
| 59 | type p1 = __ |
---|
| 60 | |
---|
| 61 | (** val p2 : sigma -> p1 **) |
---|
| 62 | let p2 s = |
---|
| 63 | let x = s in x |
---|
| 64 | |
---|
| 65 | (** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **) |
---|
| 66 | let rec jmeq_rect_Type4 x h_refl_jmeq x_929 = |
---|
| 67 | h_refl_jmeq |
---|
| 68 | |
---|
| 69 | (** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **) |
---|
| 70 | let rec jmeq_rect_Type5 x h_refl_jmeq x_932 = |
---|
| 71 | h_refl_jmeq |
---|
| 72 | |
---|
| 73 | (** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **) |
---|
| 74 | let rec jmeq_rect_Type3 x h_refl_jmeq x_935 = |
---|
| 75 | h_refl_jmeq |
---|
| 76 | |
---|
| 77 | (** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **) |
---|
| 78 | let rec jmeq_rect_Type2 x h_refl_jmeq x_938 = |
---|
| 79 | h_refl_jmeq |
---|
| 80 | |
---|
| 81 | (** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **) |
---|
| 82 | let rec jmeq_rect_Type1 x h_refl_jmeq x_941 = |
---|
| 83 | h_refl_jmeq |
---|
| 84 | |
---|
| 85 | (** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **) |
---|
| 86 | let rec jmeq_rect_Type0 x h_refl_jmeq x_944 = |
---|
| 87 | h_refl_jmeq |
---|
| 88 | |
---|
| 89 | (** val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **) |
---|
| 90 | let jmeq_inv_rect_Type4 x2 x4 h1 = |
---|
| 91 | let hcut = jmeq_rect_Type4 x2 h1 x4 in hcut __ __ |
---|
| 92 | |
---|
| 93 | (** val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **) |
---|
| 94 | let jmeq_inv_rect_Type3 x2 x4 h1 = |
---|
| 95 | let hcut = jmeq_rect_Type3 x2 h1 x4 in hcut __ __ |
---|
| 96 | |
---|
| 97 | (** val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **) |
---|
| 98 | let jmeq_inv_rect_Type2 x2 x4 h1 = |
---|
| 99 | let hcut = jmeq_rect_Type2 x2 h1 x4 in hcut __ __ |
---|
| 100 | |
---|
| 101 | (** val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **) |
---|
| 102 | let jmeq_inv_rect_Type1 x2 x4 h1 = |
---|
| 103 | let hcut = jmeq_rect_Type1 x2 h1 x4 in hcut __ __ |
---|
| 104 | |
---|
| 105 | (** val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **) |
---|
| 106 | let jmeq_inv_rect_Type0 x2 x4 h1 = |
---|
| 107 | let hcut = jmeq_rect_Type0 x2 h1 x4 in hcut __ __ |
---|
| 108 | |
---|
| 109 | (** val jmeq_discr : 'a1 -> 'a2 -> __ **) |
---|
| 110 | let jmeq_discr a2 a4 = |
---|
| 111 | Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __ |
---|
| 112 | |
---|
| 113 | (** val cast : 'a1 -> 'a2 **) |
---|
| 114 | let cast x = |
---|
| 115 | (fun x0 -> Obj.magic x0) x |
---|
| 116 | |
---|
| 117 | type ('a, 'x) curry = 'x |
---|
| 118 | |
---|
| 119 | (** val g : 'a1 -> 'a2 -> 'a1 -> 'a2 **) |
---|
| 120 | let g x h y = |
---|
| 121 | (fun _ -> Logic.eq_rect_Type0 __ h __) __ |
---|
| 122 | |
---|
| 123 | type 'p pP = 'p |
---|
| 124 | |
---|
| 125 | (** val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP **) |
---|
| 126 | let e a h b = |
---|
| 127 | let x = g a h b in x |
---|
| 128 | |
---|
| 129 | (** val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 **) |
---|
| 130 | let jmeq_elim x x0 y = |
---|
| 131 | e x x0 y |
---|
| 132 | |
---|