1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode_base_lemmas_instrmode1.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma
index aa1f4579c0386719ea962321da4f0c8e78445b70..ad383d2ab72567b38e03afbee6e8b7d285bbaff0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/aux_bases_lemmas.ma".
@@ -39,11 +35,11 @@ ndefinition instr_mode_destruct1 :
  nnormalize;
  ##[ ##1: #H; napply (λx:P.x)
  ##| ##2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -56,11 +52,11 @@ ndefinition instr_mode_destruct2 :
  nnormalize;
  ##[ ##2: #H; napply (λx:P.x)
  ##| ##1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -73,11 +69,11 @@ ndefinition instr_mode_destruct3 :
  nnormalize;
  ##[ ##3: #H; napply (λx:P.x)
  ##| ##1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -90,11 +86,11 @@ ndefinition instr_mode_destruct4 :
  nnormalize;
  ##[ ##4: #H; napply (λx:P.x)
  ##| ##1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -107,11 +103,11 @@ ndefinition instr_mode_destruct5 :
  nnormalize;
  ##[ ##5: #H; napply (λx:P.x)
  ##| ##1,2,3,4,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -124,11 +120,11 @@ ndefinition instr_mode_destruct6 :
  nnormalize;
  ##[ ##6: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -141,11 +137,11 @@ ndefinition instr_mode_destruct7 :
  nnormalize;
  ##[ ##7: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -158,11 +154,11 @@ ndefinition instr_mode_destruct8 :
  nnormalize;
  ##[ ##8: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -175,11 +171,11 @@ ndefinition instr_mode_destruct9 :
  nnormalize;
  ##[ ##9: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -192,11 +188,11 @@ ndefinition instr_mode_destruct10 :
  nnormalize;
  ##[ ##10: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -209,11 +205,11 @@ ndefinition instr_mode_destruct11 :
  nnormalize;
  ##[ ##11: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -226,11 +222,11 @@ ndefinition instr_mode_destruct12 :
  nnormalize;
  ##[ ##12: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -243,11 +239,11 @@ ndefinition instr_mode_destruct13 :
  nnormalize;
  ##[ ##13: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -260,11 +256,11 @@ ndefinition instr_mode_destruct14 :
  nnormalize;
  ##[ ##14: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -277,11 +273,11 @@ ndefinition instr_mode_destruct15 :
  nnormalize;
  ##[ ##15: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -294,11 +290,11 @@ ndefinition instr_mode_destruct16 :
  nnormalize;
  ##[ ##16: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -311,11 +307,11 @@ ndefinition instr_mode_destruct17 :
  nnormalize;
  ##[ ##17: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -328,11 +324,11 @@ ndefinition instr_mode_destruct18 :
  nnormalize;
  ##[ ##18: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -345,11 +341,11 @@ ndefinition instr_mode_destruct19 :
  nnormalize;
  ##[ ##19: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -362,11 +358,11 @@ ndefinition instr_mode_destruct20 :
  nnormalize;
  ##[ ##20: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -379,11 +375,11 @@ ndefinition instr_mode_destruct21 :
  nnormalize;
  ##[ ##21: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -396,11 +392,11 @@ ndefinition instr_mode_destruct22 :
  nnormalize;
  ##[ ##22: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -413,11 +409,11 @@ ndefinition instr_mode_destruct23 :
  nnormalize;
  ##[ ##23: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -430,11 +426,11 @@ ndefinition instr_mode_destruct24 :
  nnormalize;
  ##[ ##24: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -447,11 +443,11 @@ ndefinition instr_mode_destruct25 :
  nnormalize;
  ##[ ##25: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -464,11 +460,11 @@ ndefinition instr_mode_destruct26 :
  nnormalize;
  ##[ ##26: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -481,11 +477,11 @@ ndefinition instr_mode_destruct27 :
  nnormalize;
  ##[ ##27: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -498,11 +494,11 @@ ndefinition instr_mode_destruct28 :
  nnormalize;
  ##[ ##28: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -515,11 +511,11 @@ ndefinition instr_mode_destruct29 :
  nnormalize;
  ##[ ##29: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -532,11 +528,11 @@ ndefinition instr_mode_destruct30 :
  nnormalize;
  ##[ ##30: #H; napply (λx:P.x)
  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##]
@@ -547,7 +543,7 @@ nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 →
  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct31 :
@@ -563,11 +559,11 @@ ndefinition instr_mode_destruct31 :
  ncases i2;
  nnormalize;
  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##32,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31: #n2;
@@ -575,7 +571,7 @@ ndefinition instr_mode_destruct31 :
      ncases n2;
      nnormalize;
      ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn ?? H))
+     ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn … H))
      ##]
 nqed.
 
@@ -584,7 +580,7 @@ nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 =
  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct32 :
@@ -600,11 +596,11 @@ ndefinition instr_mode_destruct32 :
  ncases i2;
  nnormalize;
  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,33,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##32: #n2;
@@ -612,7 +608,7 @@ ndefinition instr_mode_destruct32 :
      ncases n2;
      nnormalize;
      ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H))
+     ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn_and_IMM1 … H))
      ##]
 nqed.
 
@@ -621,7 +617,7 @@ nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1
  nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct33 :
@@ -641,11 +637,11 @@ ndefinition instr_mode_destruct33 :
  ncases i2;
  nnormalize;
  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,34: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##33: #n2;
@@ -653,7 +649,7 @@ ndefinition instr_mode_destruct33 :
      ncases n2;
      nnormalize;
      ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (exadecim_destruct ??? (instr_mode_destruct_MODE_TNY ?? H))
+     ##| ##*: #H; napply (exadecim_destruct … (instr_mode_destruct_MODE_TNY … H))
      ##]
 nqed.
 
@@ -662,7 +658,7 @@ nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1
  nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct34 :
@@ -690,142 +686,142 @@ ndefinition instr_mode_destruct34 :
  ncases i2;
  nnormalize;
  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##31,32,33: #n; #H;
-     napply (False_ind ??);
+     napply (False_ind (λ_.?) ?);
      nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
      nrewrite > H; nnormalize; napply I
  ##| ##34: #n2;
      ncases n1;
      ##[ ##1: ncases n2; nnormalize;
               ##[ ##1: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##2: ncases n2; nnormalize;
               ##[ ##2: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##3: ncases n2; nnormalize;
               ##[ ##3: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##4: ncases n2; nnormalize;
               ##[ ##4: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##5: ncases n2; nnormalize;
               ##[ ##5: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##6: ncases n2; nnormalize;
               ##[ ##6: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##7: ncases n2; nnormalize;
               ##[ ##7: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##8: ncases n2; nnormalize;
               ##[ ##8: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##9: ncases n2; nnormalize;
               ##[ ##9: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##10: ncases n2; nnormalize;
               ##[ ##10: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##11: ncases n2; nnormalize;
               ##[ ##11: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##12: ncases n2; nnormalize;
               ##[ ##12: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##13: ncases n2; nnormalize;
               ##[ ##13: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##14: ncases n2; nnormalize;
               ##[ ##14: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##15: ncases n2; nnormalize;
               ##[ ##15: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##16: ncases n2; nnormalize;
               ##[ ##16: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##17: ncases n2; nnormalize;
               ##[ ##17: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##18: ncases n2; nnormalize;
               ##[ ##18: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##19: ncases n2; nnormalize;
               ##[ ##19: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##20: ncases n2; nnormalize;
               ##[ ##20: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##21: ncases n2; nnormalize;
               ##[ ##21: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##22: ncases n2; nnormalize;
               ##[ ##22: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##23: ncases n2; nnormalize;
               ##[ ##23: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##24: ncases n2; nnormalize;
               ##[ ##24: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##25: ncases n2; nnormalize;
               ##[ ##25: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##26: ncases n2; nnormalize;
               ##[ ##26: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##27: ncases n2; nnormalize;
               ##[ ##27: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##28: ncases n2; nnormalize;
               ##[ ##28: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##29: ncases n2; nnormalize;
               ##[ ##29: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##30: ncases n2; nnormalize;
               ##[ ##30: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##31: ncases n2; nnormalize;
               ##[ ##31: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##32: ncases n2; nnormalize;
               ##[ ##32: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##]
  ##]