helm/software/matita/contribs/ng_assembly/common/meta_type.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/string_lemmas.ma".
  24
  25 nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  26  match l with
  27   [ nil ⇒ true
  28   | cons h t ⇒ match f elem h with
  29    [ true ⇒ false | false ⇒ nmember_list T elem f t ]
  30   ].
  31
  32 (* elem presente una ed una sola volta in l *)
  33 nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  34  match l with
  35   [ nil ⇒ false
  36   | cons h t ⇒ match f elem h with
  37     [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
  38   ].
  39
  40 (* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
  41 ninductive UN : Type ≝
  42 (* quaternari[4] 1-4 *)
  43   uq0 : UN
  44 | uq1 : UN
  45 | uq2 : UN
  46 | uq3 : UN
  47
  48 (* ottali[8] 5-12 *)
  49 | uo0 : UN
  50 | uo1 : UN
  51 | uo2 : UN
  52 | uo3 : UN
  53 | uo4 : UN
  54 | uo5 : UN
  55 | uo6 : UN
  56 | uo7 : UN
  57
  58 (* esadecimali[16] 13-28 *)
  59 | ux0 : UN
  60 | ux1 : UN
  61 | ux2 : UN
  62 | ux3 : UN
  63 | ux4 : UN
  64 | ux5 : UN
  65 | ux6 : UN
  66 | ux7 : UN
  67 | ux8 : UN
  68 | ux9 : UN
  69 | uxA : UN
  70 | uxB : UN
  71 | uxC : UN
  72 | uxD : UN
  73 | uxE : UN
  74 | uxF : UN
  75
  76 (* bitrigesimali[32] 29-60 *)
  77 | ut00 : UN
  78 | ut01 : UN
  79 | ut02 : UN
  80 | ut03 : UN
  81 | ut04 : UN
  82 | ut05 : UN
  83 | ut06 : UN
  84 | ut07 : UN
  85 | ut08 : UN
  86 | ut09 : UN
  87 | ut0A : UN
  88 | ut0B : UN
  89 | ut0C : UN
  90 | ut0D : UN
  91 | ut0E : UN
  92 | ut0F : UN
  93 | ut10 : UN
  94 | ut11 : UN
  95 | ut12 : UN
  96 | ut13 : UN
  97 | ut14 : UN
  98 | ut15 : UN
  99 | ut16 : UN
 100 | ut17 : UN
 101 | ut18 : UN
 102 | ut19 : UN
 103 | ut1A : UN
 104 | ut1B : UN
 105 | ut1C : UN
 106 | ut1D : UN
 107 | ut1E : UN
 108 | ut1F : UN
 109
 110 (* ascii[63] 61-123 *)
 111 | uch_0 : UN
 112 | uch_1 : UN
 113 | uch_2 : UN
 114 | uch_3 : UN
 115 | uch_4 : UN
 116 | uch_5 : UN
 117 | uch_6 : UN
 118 | uch_7 : UN
 119 | uch_8 : UN
 120 | uch_9 : UN
 121 | uch__ : UN
 122 | uch_A : UN
 123 | uch_B : UN
 124 | uch_C : UN
 125 | uch_D : UN
 126 | uch_E : UN
 127 | uch_F : UN
 128 | uch_G : UN
 129 | uch_H : UN
 130 | uch_I : UN
 131 | uch_J : UN
 132 | uch_K : UN
 133 | uch_L : UN
 134 | uch_M : UN
 135 | uch_N : UN
 136 | uch_O : UN
 137 | uch_P : UN
 138 | uch_Q : UN
 139 | uch_R : UN
 140 | uch_S : UN
 141 | uch_T : UN
 142 | uch_U : UN
 143 | uch_V : UN
 144 | uch_W : UN
 145 | uch_X : UN
 146 | uch_Y : UN
 147 | uch_Z : UN
 148 | uch_a : UN
 149 | uch_b : UN
 150 | uch_c : UN
 151 | uch_d : UN
 152 | uch_e : UN
 153 | uch_f : UN
 154 | uch_g : UN
 155 | uch_h : UN
 156 | uch_i : UN
 157 | uch_j : UN
 158 | uch_k : UN
 159 | uch_l : UN
 160 | uch_m : UN
 161 | uch_n : UN
 162 | uch_o : UN
 163 | uch_p : UN
 164 | uch_q : UN
 165 | uch_r : UN
 166 | uch_s : UN
 167 | uch_t : UN
 168 | uch_u : UN
 169 | uch_v : UN
 170 | uch_w : UN
 171 | uch_x : UN
 172 | uch_y : UN
 173 | uch_z : UN
 174
 175 (* opcode[91] 124-214 *)
 176 | ADC    : UN
 177 | ADD    : UN
 178 | AIS    : UN
 179 | AIX    : UN
 180 | AND    : UN
 181 | ASL    : UN
 182 | ASR    : UN
 183 | BCC    : UN
 184 | BCLRn  : UN
 185 | BCS    : UN
 186 | BEQ    : UN
 187 | BGE    : UN
 188 | BGND   : UN
 189 | BGT    : UN
 190 | BHCC   : UN
 191 | BHCS   : UN
 192 | BHI    : UN
 193 | BIH    : UN
 194 | BIL    : UN
 195 | BIT    : UN
 196 | BLE    : UN
 197 | BLS    : UN
 198 | BLT    : UN
 199 | BMC    : UN
 200 | BMI    : UN
 201 | BMS    : UN
 202 | BNE    : UN
 203 | BPL    : UN
 204 | BRA    : UN
 205 | BRCLRn : UN
 206 | BRN    : UN
 207 | BRSETn : UN
 208 | BSETn  : UN
 209 | BSR    : UN
 210 | CBEQA  : UN
 211 | CBEQX  : UN
 212 | CLC    : UN
 213 | CLI    : UN
 214 | CLR    : UN
 215 | CMP    : UN
 216 | COM    : UN
 217 | CPHX   : UN
 218 | CPX    : UN
 219 | DAA    : UN
 220 | DBNZ   : UN
 221 | DEC    : UN
 222 | DIV    : UN
 223 | EOR    : UN
 224 | INC    : UN
 225 | JMP    : UN
 226 | JSR    : UN
 227 | LDA    : UN
 228 | LDHX   : UN
 229 | LDX    : UN
 230 | LSR    : UN
 231 | MOV    : UN
 232 | MUL    : UN
 233 | NEG    : UN
 234 | NOP    : UN
 235 | NSA    : UN
 236 | ORA    : UN
 237 | PSHA   : UN
 238 | PSHH   : UN
 239 | PSHX   : UN
 240 | PULA   : UN
 241 | PULH   : UN
 242 | PULX   : UN
 243 | ROL    : UN
 244 | ROR    : UN
 245 | RSP    : UN
 246 | RTI    : UN
 247 | RTS    : UN
 248 | SBC    : UN
 249 | SEC    : UN
 250 | SEI    : UN
 251 | SHA    : UN
 252 | SLA    : UN
 253 | STA    : UN
 254 | STHX   : UN
 255 | STOP   : UN
 256 | STX    : UN
 257 | SUB    : UN
 258 | SWI    : UN
 259 | TAP    : UN
 260 | TAX    : UN
 261 | TPA    : UN
 262 | TST    : UN
 263 | TSX    : UN
 264 | TXA    : UN
 265 | TXS    : UN
 266 | WAIT   : UN
 267 .
 268
 269 (* funzione di uguaglianza sugli atomi *)
 270 ndefinition eq_UN ≝
 271 λu1,u2.match u1 with
 272  [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
 273  | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
 274  | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
 275  | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
 276
 277  | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
 278  | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
 279  | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
 280  | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
 281  | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
 282  | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
 283  | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
 284  | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
 285
 286  | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
 287  | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
 288  | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
 289  | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
 290  | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
 291  | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
 292  | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
 293  | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
 294  | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
 295  | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
 296  | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
 297  | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
 298  | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
 299  | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
 300  | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
 301  | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
 302
 303  | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ]
 304  | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ]
 305  | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ]
 306  | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ]
 307  | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ]
 308  | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ]
 309  | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ]
 310  | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ]
 311  | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ]
 312  | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ]
 313  | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ]
 314  | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ]
 315  | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ]
 316  | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ]
 317  | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ]
 318  | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ]
 319  | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ]
 320  | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ]
 321  | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ]
 322  | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ]
 323  | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ]
 324  | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ]
 325  | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ]
 326  | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ]
 327  | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ]
 328  | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ]
 329  | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ]
 330  | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ]
 331  | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ]
 332  | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ]
 333  | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ]
 334  | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ]
 335
 336  | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ]
 337  | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ]
 338  | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ]
 339  | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ]
 340  | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ]
 341  | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ]
 342  | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ]
 343  | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ]
 344  | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ]
 345  | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ]
 346  | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ]
 347  | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ]
 348  | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ]
 349  | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ]
 350  | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ]
 351  | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ]
 352  | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ]
 353  | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ]
 354  | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ]
 355  | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ]
 356  | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ]
 357  | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ]
 358  | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ]
 359  | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ]
 360  | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ]
 361  | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ]
 362  | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ]
 363  | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ]
 364  | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ]
 365  | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ]
 366  | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ]
 367  | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ]
 368  | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ]
 369  | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ]
 370  | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ]
 371  | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ]
 372  | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ]
 373  | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ]
 374  | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ]
 375  | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ]
 376  | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ]
 377  | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ]
 378  | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ]
 379  | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ]
 380  | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ]
 381  | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ]
 382  | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ]
 383  | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ]
 384  | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ]
 385  | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ]
 386  | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ]
 387  | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ]
 388  | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ]
 389  | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ]
 390  | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ]
 391  | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ]
 392  | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ]
 393  | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ]
 394  | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ]
 395  | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ]
 396  | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ]
 397  | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ]
 398  | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ]
 399
 400  | ADC    ⇒ match u2 with [ ADC    ⇒ true | _ ⇒ false ]
 401  | ADD    ⇒ match u2 with [ ADD    ⇒ true | _ ⇒ false ]
 402  | AIS    ⇒ match u2 with [ AIS    ⇒ true | _ ⇒ false ]
 403  | AIX    ⇒ match u2 with [ AIX    ⇒ true | _ ⇒ false ]
 404  | AND    ⇒ match u2 with [ AND    ⇒ true | _ ⇒ false ]
 405  | ASL    ⇒ match u2 with [ ASL    ⇒ true | _ ⇒ false ]
 406  | ASR    ⇒ match u2 with [ ASR    ⇒ true | _ ⇒ false ]
 407  | BCC    ⇒ match u2 with [ BCC    ⇒ true | _ ⇒ false ]
 408  | BCLRn  ⇒ match u2 with [ BCLRn  ⇒ true | _ ⇒ false ]
 409  | BCS    ⇒ match u2 with [ BCS    ⇒ true | _ ⇒ false ]
 410  | BEQ    ⇒ match u2 with [ BEQ    ⇒ true | _ ⇒ false ]
 411  | BGE    ⇒ match u2 with [ BGE    ⇒ true | _ ⇒ false ]
 412  | BGND   ⇒ match u2 with [ BGND   ⇒ true | _ ⇒ false ]
 413  | BGT    ⇒ match u2 with [ BGT    ⇒ true | _ ⇒ false ]
 414  | BHCC   ⇒ match u2 with [ BHCC   ⇒ true | _ ⇒ false ]
 415  | BHCS   ⇒ match u2 with [ BHCS   ⇒ true | _ ⇒ false ]
 416  | BHI    ⇒ match u2 with [ BHI    ⇒ true | _ ⇒ false ]
 417  | BIH    ⇒ match u2 with [ BIH    ⇒ true | _ ⇒ false ]
 418  | BIL    ⇒ match u2 with [ BIL    ⇒ true | _ ⇒ false ]
 419  | BIT    ⇒ match u2 with [ BIT    ⇒ true | _ ⇒ false ]
 420  | BLE    ⇒ match u2 with [ BLE    ⇒ true | _ ⇒ false ]
 421  | BLS    ⇒ match u2 with [ BLS    ⇒ true | _ ⇒ false ]
 422  | BLT    ⇒ match u2 with [ BLT    ⇒ true | _ ⇒ false ]
 423  | BMC    ⇒ match u2 with [ BMC    ⇒ true | _ ⇒ false ]
 424  | BMI    ⇒ match u2 with [ BMI    ⇒ true | _ ⇒ false ]
 425  | BMS    ⇒ match u2 with [ BMS    ⇒ true | _ ⇒ false ]
 426  | BNE    ⇒ match u2 with [ BNE    ⇒ true | _ ⇒ false ]
 427  | BPL    ⇒ match u2 with [ BPL    ⇒ true | _ ⇒ false ]
 428  | BRA    ⇒ match u2 with [ BRA    ⇒ true | _ ⇒ false ]
 429  | BRCLRn ⇒ match u2 with [ BRCLRn ⇒ true | _ ⇒ false ]
 430  | BRN    ⇒ match u2 with [ BRN    ⇒ true | _ ⇒ false ]
 431  | BRSETn ⇒ match u2 with [ BRSETn ⇒ true | _ ⇒ false ]
 432  | BSETn  ⇒ match u2 with [ BSETn  ⇒ true | _ ⇒ false ]
 433  | BSR    ⇒ match u2 with [ BSR    ⇒ true | _ ⇒ false ]
 434  | CBEQA  ⇒ match u2 with [ CBEQA  ⇒ true | _ ⇒ false ]
 435  | CBEQX  ⇒ match u2 with [ CBEQX  ⇒ true | _ ⇒ false ]
 436  | CLC    ⇒ match u2 with [ CLC    ⇒ true | _ ⇒ false ]
 437  | CLI    ⇒ match u2 with [ CLI    ⇒ true | _ ⇒ false ]
 438  | CLR    ⇒ match u2 with [ CLR    ⇒ true | _ ⇒ false ]
 439  | CMP    ⇒ match u2 with [ CMP    ⇒ true | _ ⇒ false ]
 440  | COM    ⇒ match u2 with [ COM    ⇒ true | _ ⇒ false ]
 441  | CPHX   ⇒ match u2 with [ CPHX   ⇒ true | _ ⇒ false ]
 442  | CPX    ⇒ match u2 with [ CPX    ⇒ true | _ ⇒ false ]
 443  | DAA    ⇒ match u2 with [ DAA    ⇒ true | _ ⇒ false ]
 444  | DBNZ   ⇒ match u2 with [ DBNZ   ⇒ true | _ ⇒ false ]
 445  | DEC    ⇒ match u2 with [ DEC    ⇒ true | _ ⇒ false ]
 446  | DIV    ⇒ match u2 with [ DIV    ⇒ true | _ ⇒ false ]
 447  | EOR    ⇒ match u2 with [ EOR    ⇒ true | _ ⇒ false ]
 448  | INC    ⇒ match u2 with [ INC    ⇒ true | _ ⇒ false ]
 449  | JMP    ⇒ match u2 with [ JMP    ⇒ true | _ ⇒ false ]
 450  | JSR    ⇒ match u2 with [ JSR    ⇒ true | _ ⇒ false ]
 451  | LDA    ⇒ match u2 with [ LDA    ⇒ true | _ ⇒ false ]
 452  | LDHX   ⇒ match u2 with [ LDHX   ⇒ true | _ ⇒ false ]
 453  | LDX    ⇒ match u2 with [ LDX    ⇒ true | _ ⇒ false ]
 454  | LSR    ⇒ match u2 with [ LSR    ⇒ true | _ ⇒ false ]
 455  | MOV    ⇒ match u2 with [ MOV    ⇒ true | _ ⇒ false ]
 456  | MUL    ⇒ match u2 with [ MUL    ⇒ true | _ ⇒ false ]
 457  | NEG    ⇒ match u2 with [ NEG    ⇒ true | _ ⇒ false ]
 458  | NOP    ⇒ match u2 with [ NOP    ⇒ true | _ ⇒ false ]
 459  | NSA    ⇒ match u2 with [ NSA    ⇒ true | _ ⇒ false ]
 460  | ORA    ⇒ match u2 with [ ORA    ⇒ true | _ ⇒ false ]
 461  | PSHA   ⇒ match u2 with [ PSHA   ⇒ true | _ ⇒ false ]
 462  | PSHH   ⇒ match u2 with [ PSHH   ⇒ true | _ ⇒ false ]
 463  | PSHX   ⇒ match u2 with [ PSHX   ⇒ true | _ ⇒ false ]
 464  | PULA   ⇒ match u2 with [ PULA   ⇒ true | _ ⇒ false ]
 465  | PULH   ⇒ match u2 with [ PULH   ⇒ true | _ ⇒ false ]
 466  | PULX   ⇒ match u2 with [ PULX   ⇒ true | _ ⇒ false ]
 467  | ROL    ⇒ match u2 with [ ROL    ⇒ true | _ ⇒ false ]
 468  | ROR    ⇒ match u2 with [ ROR    ⇒ true | _ ⇒ false ]
 469  | RSP    ⇒ match u2 with [ RSP    ⇒ true | _ ⇒ false ]
 470  | RTI    ⇒ match u2 with [ RTI    ⇒ true | _ ⇒ false ]
 471  | RTS    ⇒ match u2 with [ RTS    ⇒ true | _ ⇒ false ]
 472  | SBC    ⇒ match u2 with [ SBC    ⇒ true | _ ⇒ false ]
 473  | SEC    ⇒ match u2 with [ SEC    ⇒ true | _ ⇒ false ]
 474  | SEI    ⇒ match u2 with [ SEI    ⇒ true | _ ⇒ false ]
 475  | SHA    ⇒ match u2 with [ SHA    ⇒ true | _ ⇒ false ]
 476  | SLA    ⇒ match u2 with [ SLA    ⇒ true | _ ⇒ false ]
 477  | STA    ⇒ match u2 with [ STA    ⇒ true | _ ⇒ false ]
 478  | STHX   ⇒ match u2 with [ STHX   ⇒ true | _ ⇒ false ]
 479  | STOP   ⇒ match u2 with [ STOP   ⇒ true | _ ⇒ false ]
 480  | STX    ⇒ match u2 with [ STX    ⇒ true | _ ⇒ false ]
 481  | SUB    ⇒ match u2 with [ SUB    ⇒ true | _ ⇒ false ]
 482  | SWI    ⇒ match u2 with [ SWI    ⇒ true | _ ⇒ false ]
 483  | TAP    ⇒ match u2 with [ TAP    ⇒ true | _ ⇒ false ]
 484  | TAX    ⇒ match u2 with [ TAX    ⇒ true | _ ⇒ false ]
 485  | TPA    ⇒ match u2 with [ TPA    ⇒ true | _ ⇒ false ]
 486  | TST    ⇒ match u2 with [ TST    ⇒ true | _ ⇒ false ]
 487  | TSX    ⇒ match u2 with [ TSX    ⇒ true | _ ⇒ false ]
 488  | TXA    ⇒ match u2 with [ TXA    ⇒ true | _ ⇒ false ]
 489  | TXS    ⇒ match u2 with [ TXS    ⇒ true | _ ⇒ false ]
 490  | WAIT   ⇒ match u2 with [ WAIT   ⇒ true | _ ⇒ false ]
 491
 492  ].
 493
 494 ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P  | false ⇒ P ].
 495  #x; #y; #P; #H;
 496  nrewrite > H;
 497  nelim y;
 498  nnormalize;
 499  napply (λx.x).
 500 nqed.
 501
 502 nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
 503  #e1; #e2; #H;
 504  nrewrite > H;
 505  nelim e2;
 506  nnormalize;
 507  napply refl_eq.
 508 nqed.
 509
 510 nlemma pippo : ∀A,B:Prop.(A → B) → ((¬B) → (¬A)).
 511  #A; #B; #H; nnormalize;
 512  #H1; #H2;
 513  napply (H1 (H H2)).
 514 nqed.
 515
 516 nlemma pluto1 : ∀x.x = false → x ≠ true.
 517  #x; nelim x;
 518  ##[ ##1: #H; napply (bool_destruct … H)
 519  ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
 520  ##]
 521 nqed.
 522
 523 nlemma pluto2 : ∀x.x = true → x ≠ false.
 524  #x; nelim x;
 525  ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
 526  ##| ##2: #H; napply (bool_destruct … H)
 527  ##]
 528 nqed.
 529
 530 nlemma pluto3 : ∀x.x ≠ false → x = true.
 531  #x; nelim x;
 532  ##[ ##1: #H; napply refl_eq
 533  ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
 534  ##]
 535 nqed.
 536
 537 nlemma pluto4 : ∀x.x ≠ true → x = false.
 538  #x; nelim x;
 539  ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
 540  ##| ##2: #H; napply refl_eq
 541  ##]
 542 nqed.
 543
 544 nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
 545  #e1; #e2; #H;
 546  napply (pippo (e1 = e2) (eq_UN e1 e2 = true) …);
 547  ##[ ##1: napply (eq_to_eqUN e1 e2)
 548  ##| ##2: napply (pluto1 … H)
 549  ##]
 550 nqed.
 551
 552 naxiom eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
 553
 554 nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
 555  #e1; #e2; #H;
 556  napply (pluto4 (eq_UN e1 e2));
 557  napply (pippo (eq_UN e1 e2 = true) (e1 = e2) ? H);
 558  napply (eqUN_to_eq e1 e2).
 559 nqed.
 560
 561 nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
 562  #x; #y; nnormalize;
 563  napply (or2_elim (eq_UN x y = true) (eq_UN x y = false) ?);
 564  ##[ ##1: ncases (eq_UN x y);
 565           ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
 566           ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
 567           ##]
 568  ##| ##2: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqUN_to_eq … H))
 569  ##| ##3: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqUN_to_neq … H))
 570  ##]
 571 nqed.
 572
 573  nrewrite > (eq_to_eqUN e1 e2 ?);
 574
 575 nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
 576  #e1; #e2; #H;
 577
 578
 579 nlemma pippo : ∀P.(¬¬¬P) → (¬P).
 580  #P; nnormalize; #H; #H1;
 581  napply H; #H2;
 582  napply (H2 H1).
 583 nqed.
 584
 585 nlemma pippo2 : ∀P.(¬¬P) → P.
 586  #P; nnormalize; #H;
 587  napply (or2_elim (¬P) (¬¬¬¬P) ?);
 588  ##[ ##1: napply (or2_intro2 ?? (prop_to_nnprop ? H))
 589  ##| ##2: #H1; nelim (H H1)
 590  ##| ##3: #H1; napply False_ind;
 591           napply (H (pippo …));
 592           nnormalize; #H2;
 593           napply False_ind;
 594           napply (pippo ? H1);
 595           #H2;
 596           napply H;
 597           napply False_ind;
 598           napply H1; #H2;
 599
 600  ##[ ##2: #H1;napply (prop_to_nnprop ? H);
 601  ##| ##1: nnormalize; #H1;
 602  napply False_ind;
 603  napply H; #H1;
 604  napply H;
 605  napply (or2_elim (¬¬P) (¬¬¬P) ?);
 606  ##[ ##1: napply (or2_intro1 ?? H);
 607
 608  napply (absurd (¬¬¬P) P ??);
 609  ##[ ##2: napply (prop_to_nnprop ? H);
 610  ##| ##1:
 611  napply (pippo P);
 612  nnormalize;
 613  nnormalize in H:(%);
 614  #H1;
 615  #H1;
 616  napply (absurd ? False H ?);
 617  nnormalize;
 618  #H2;
 619  nnormalize; #H;
 620  napply False_ind;
 621  napply H; #H1;
 622  napply (absurd ? False (prop_to_nnprop (¬P) ?));
 623  ##[ ##1: nnormalize; #H2; napply (H2 H)
 624  ##| ##2:
 625  nnormalize; #H2;
 626  nnormalize in K:(%);
 627  # .
 628 nqed.
 629
 630 nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
 631  #e1; #e2;
 632  napply (or2_elim (eq_UN e1 e2 = false) (e1 ≠ e2) ?);
 633  ##[ ##3:
 634  nelim e1;
 635  nnormalize;
 636  nchange with (match e2 with [ ? ⇒ true | _ ⇒ false ]);
 637  nelim e2;
 638  #H;
 639  napply (or2_elim (e1 = e2) (e1 ≠ e2) …);
 640  ##[ ##2:
 641
 642  ##[ ##1: ncases (eq_UN e1 e2);
 643           ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
 644           ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
 645           ##]
 646  ##| ##3:
 647
 648
 649  nnormalize;
 650  nrewrite > H;
 651  nelim e2;
 652  nnormalize;
 653  napply refl_eq.
 654 nqed.
 655
 656 ndefinition decidable_UN1 ≝ λx.∀y:UN.decidable (x = y).
 657  #x;
 658  nnormalize;
 659  nelim x;
 660  ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 661  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (UN_destruct … H)
 662  ##]
 663 nqed.
 664
 665 naxiom decidable_UN : ∀x,y:UN.decidable (x = y).
 666
 667 nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
 668  #e1; #e2; #H;
 669
 670 nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
 671  #e1; #e2; #H; napply (or2_elim ??? (decidable_UN e1 e2));
 672  ##[ ##2: #H1;
 673
 674 nlemma pippo : ∀e1,e2:UN.decidable (e1 = e2).
 675  #e1; #e2; nnormalize;
 676  nelim e1;
 677  napply (or2_intro1 (? = ?) (? ≠ ?) …);
 678  nchange with (match e2 with [ ? ⇒ refl_eq UN ? | _ ⇒ ? ]);
 679  napply (destruct_UN ? e2 (? = e2) ?);
 680
 681 nlemma pippo : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
 682  #e1; nelim e1; #e2;
 683
 684
 685 (* costruttore di un sottouniverso:
 686    S_EL cioe' uno qualsiasi degli elementi del sottouniverso
 687    S_KO cioe' il caso impossibile
 688 *)
 689 ninductive S_UN (l:list UN) : Type ≝
 690   S_EL : Πx:UN.((member_list UN x eq_UN l) = true) →
 691                (∀y.x = y → (eq_UN x y = true)) →
 692                (∀y.(eq_UN x y = true) → x = y) →
 693                (∀y.decidable (x = y)) →
 694                (∀y.x ≠ y → (eq_UN x y = false)) →
 695                (∀y.(eq_UN x y = false) → x ≠ y) →
 696                S_UN l
 697 | S_KO : False → S_UN l.
 698
 699 ndefinition SUN_create : Πl.Πe.(member_list UN e eq_UN l = true) → S_UN l.
 700  #l; #e; #dim; napply (S_EL l e dim …);
 701  ##[ ##1: #y; #H; nrewrite > H; nelim y; nnormalize; napply refl_eq
 702  ##| ##2: #y;
 703
 704 (* sottoinsieme degli esadecimali *)
 705 ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
 706
 707 (* getter del testimone di esistenza *)
 708 ndefinition getelem : ∀l.∀e:S_UN l.UN.
 709  #l; #s; nelim s;
 710  ##[ ##1: #u; #H; napply u
 711  ##| ##2: #H; nelim H
 712  ##]
 713 nqed.
 714
 715 (* getter della dimostrazione di appartenenza *)
 716 ndefinition getdim : ∀l.∀e:S_UN l.member_list UN ? eq_UN l = true.
 717  ##[ ##2: nelim e;
 718           ##[ ##1: #u; #H; napply u
 719           ##| ##2: #H; nelim H
 720           ##]
 721  ##| ##1: #l; #s; nelim s;
 722           ##[ ##1: #u; #m; napply m
 723           ##| ##2: #H; nelim H
 724           ##]
 725  ##]
 726 nqed.
 727
 728 (* costruttore universale di una funzione ad un solo argomento: esadecimali → esadecimali *)
 729 ndefinition f1_EX_UN
 730  : ∀e:S_UN EX_UN.
 731    ∀f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN.
 732    S_UN EX_UN.
 733  #input; #f1; #f2; #f3; #f4; #f5; #f6; #f7; #f8; #f9; #f10; #f11; #f12; #f13; #f14; #f15; #f16;
 734  nelim input;
 735  ##[ ##2: #H; nelim H
 736  ##| ##1: #u; #H; nelim u in H:(%); #H;
 737           ##[ ##13: napply f1 ##| ##14: napply f2 ##| ##15: napply f3 ##| ##16: napply f4
 738           ##| ##17: napply f5 ##| ##18: napply f6 ##| ##19: napply f7 ##| ##20: napply f8
 739           ##| ##21: napply f9 ##| ##22: napply f10 ##| ##23: napply f11 ##| ##24: napply f12
 740           ##| ##25: napply f13 ##| ##26: napply f14 ##| ##27: napply f15 ##| ##28: napply f16
 741           ##| ##*: nnormalize in H:(%); napply (S_KO EX_UN (bool_destruct false true False H))
 742           ##]
 743  ##]
 744 nqed.
 745
 746 (* esempio: successore esadecimale *)
 747 ndefinition succ_EX_UN ≝
 748 λe:S_UN EX_UN.f1_EX_UN
 749  (S_EL EX_UN ux1 (refl_eq …)) (S_EL EX_UN ux2 (refl_eq …))
 750  (S_EL EX_UN ux3 (refl_eq …)) (S_EL EX_UN ux4 (refl_eq …))
 751  (S_EL EX_UN ux5 (refl_eq …)) (S_EL EX_UN ux6 (refl_eq …))
 752  (S_EL EX_UN ux7 (refl_eq …)) (S_EL EX_UN ux8 (refl_eq …))
 753  (S_EL EX_UN ux9 (refl_eq …)) (S_EL EX_UN uxA (refl_eq …))
 754  (S_EL EX_UN uxB (refl_eq …)) (S_EL EX_UN uxC (refl_eq …))
 755  (S_EL EX_UN uxD (refl_eq …)) (S_EL EX_UN uxE (refl_eq …))
 756  (S_EL EX_UN uxF (refl_eq …)) (S_EL EX_UN ux0 (refl_eq …)).
 757
 758 (* lemmi *)
 759 nlemma same_UN_1 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
 760  #l; #e1; #e2; #dim1; #dim2; #H;
 761  nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a | S_KO _ ⇒ False ]);
 762  nrewrite < H;
 763  nnormalize;
 764  napply refl_eq.
 765 nqed.
 766
 767
 768
 769 ndefinition destruct_SUN
 770  : ∀l.∀e1,e2:S_UN l.∀P:Prop.
 771    e1 = e2 → match eq_UN (getelem ? e1) (getelem ? e2) with [ true ⇒ P → P | false ⇒ P ].
 772  #l; #e1; nelim e1;
 773  ##[ ##2: #H; nelim H
 774  ##| ##1: #u1; #dim1; #e2; ncases e2;
 775           ##[ ##2: #H; nelim H
 776           ##| ##1: #u2; #dim2; #P; #H;
 777                    nchange with (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]);
 778                    napply (destruct_UN u1 u2 P (same_UN_1 l … H))
 779           ##]
 780  ##]
 781 nqed.
 782
 783
 784
 785 nlemma eq_to_eqSUN
 786  : ∀l.∀e1,e2:S_UN l.(getelem ? e1) = (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = true.
 787  #l; #e1; nelim e1;
 788  ##[ ##2: #H; nelim H
 789  ##| ##1: #u1; #dim1; #e2; ncases e2;
 790           ##[ ##2: #H; nelim H;
 791           ##| ##1: #u2; #dim2; nchange with ((u1 = u2) → (eq_UN u1 u2 = true));
 792                    napply (eq_to_eqUN u1 u2);
 793           ##]
 794  ##]
 795 nqed.
 796
 797 nlet rec scan (T:Type) (e:T) (f:T → T → bool) (l:list T) (n:nat) on l ≝
 798  match l with
 799   [ nil ⇒ None ?
 800   | cons h t ⇒ match f e h with
 801    [ true ⇒ Some ? n
 802    | false ⇒ scan T e f t (S n)
 803    ]
 804   ].
 805
 806 nlemma pippo : ∀l.∀x,y:S_UN l.x = y → scan ? (getelem ? x) eq_UN l O = scan ? (getelem ? y) eq_UN l O.
 807  #l; nelim l;
 808  ##[ ##1: #x; #y; #H; nnormalize; napply refl_eq
 809  ##| ##2: #hh; #tt; #H; #x; nelim x;
 810           ##[ ##2: #F; nelim F
 811           ##| ##1: #u1; #dim1; #y; nelim y;
 812                    ##[ ##2: #F; nelim F
 813                    ##| ##1: #u2; #dim2; #H1;
 814                             nchange with ((scan ? u1 ???) = (scan ? u2 ???));
 815                             nrewrite > (same_UN_1 (hh::tt) … H1);
 816                             nchange with
 817                             nletin K ≝ (same_UN_1 (hh::tt) … H1);
 818                             nchange in K:(%) with (u1 = u2);
 819                             nnormalize in K:(%);
 820                             nrewrite > (same_UN_1 (hh::tt) … H1) in dim1:(%) dim2:(%) ⊢ %;
 821                             nchange with (match eq_UN
 822
 823                     nchange with (scan ? u1 eq_UN ? O = scan ? u2 eq_UN ? O);
 824
 825  #x; nelim x;
 826  ##[ ##2: #H; nelim H
 827  ##| ##1: #u1; #dim1; #y; nelim y;
 828      ##[ ##2: #H; nelim H
 829      ##| ##1: #u2; #dim2; #H; nchange with (scan ? u1 eq_UN l O = scan ? u2 eq_UN l O);
 830               nrewrite > (same_UN_1 l … H);
 831               nelim l in x:(%) dim1:(%) y:(%) dim2:(%) H:(%) ⊢ %;
 832               ##[ ##1: #x; #dim1; #y; #dim2; #H; nnormalize; napply refl_eq
 833               ##| ##2: #uu1; #ll; #H; #y;
 834               nnormalize;
 835
 836 nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
 837  #x; nnormalize; #y;
 838  napply (Or2_ind);
 839
 840
 841   napply (destruct_UN ? y (Or2 ??) ?);
 842
 843 nlemma neq_to_neqUN
 844  : ∀l.∀e1,e2:S_UN l.(getelem ? e1) ≠ (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = false.
 845  #l; #e1; nelim e1;
 846  ##[ ##2: #H; nelim H
 847  ##| ##1: #u1; #dim1; #e2; ncases e2;
 848           ##[ ##2: #H; nelim H;
 849           ##| ##1: #u2; #dim2; nchange with ((u1 ≠ u2) → (eq_UN u1 u2 = false));
 850                    #H; nrewrite > H;
 851                    nelim u2; nnormalize; napply refl_eq
 852           ##]
 853  ##]
 854 nqed.
 855
 856                    nelim u1 in dim1:(%) H:(%) ⊢ %; #dim1; #H;
 857                    ##[ ##1: nelim u2 in dim2:(%) H:(%) ⊢ %; #dim2; #H;
 858                             napply (destruct_UN l (S_EL l uq0 dim1) ?? H);
 859
 860                    ##[ ##1: nelim u2; ##[ ##1:
 861
 862
 863 ndefinition decidable_UN : ∀l.∀e1,e2:S_UN l.decidable (e1 = e2).
 864  #l; #e1; ncases e1;
 865  ##[ ##2: #H; nelim H
 866  ##| ##1: #u1; #dim1; #e2; ncases e2;
 867           ##[ ##2: #H; nelim H
 868           ##| ##1: #u2; #dim2; nnormalize;
 869                    napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 870                    nnormalize;
 871                    #H;
 872                    nchange with (match S_EL l u1 dim1
 873                                   return λx.eq_UN x u2 → Prop
 874                                  with
 875                                   [ S_EL x _ ⇒ λp:(False
 876                                   | S_KO H ⇒ True
 877                                   ] (refl_eq ? (eq_UN u1 u2);
 878                    nletin K ≝ (same_UN_1 l … H);
 879                    nelim u1 in dim1:(%) H:(%) K:(%);
 880                    #dim1; #H; #K;
 881                    napply (destruct_UN l … H);
 882
 883
 884
 885
 886
 887
 888
 889
 890
 891