freescale porting, work in progress

[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..8d8f526b7e7f08e4d04a2f582dd436bb4cf16c59 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
  ##]
@@ -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;
@@ -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;
@@ -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;
@@ -686,11 +686,11 @@ 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;