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 9ef4d01b7075e28f7df0d781edaab753da20fd1b..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
@@ -35,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
  ##]
@@ -52,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
  ##]
@@ -69,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
  ##]
@@ -86,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
  ##]
@@ -103,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
  ##]
@@ -120,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
  ##]
@@ -137,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
  ##]
@@ -154,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
  ##]
@@ -171,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
  ##]
@@ -188,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
  ##]
@@ -205,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
  ##]
@@ -222,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
  ##]
@@ -239,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
  ##]
@@ -256,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
  ##]
@@ -273,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
  ##]
@@ -290,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
  ##]
@@ -307,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
  ##]
@@ -324,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
  ##]
@@ -341,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
  ##]
@@ -358,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
  ##]
@@ -375,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
  ##]
@@ -392,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
  ##]
@@ -409,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
  ##]
@@ -426,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
  ##]
@@ -443,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
  ##]
@@ -460,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
  ##]
@@ -477,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
  ##]
@@ -494,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
  ##]
@@ -511,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
  ##]
@@ -528,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
  ##]
@@ -543,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 :
@@ -559,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;
@@ -571,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.
 
@@ -580,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 :
@@ -596,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;
@@ -608,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.
 
@@ -617,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 :
@@ -637,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;
@@ -649,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.
 
@@ -658,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 :
@@ -686,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))
               ##]
      ##]
  ##]