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 ad383d2ab72567b38e03afbee6e8b7d285bbaff0..c2e1ed6d1e89221584e7861a57c5577d6812ed95 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
@@ -20,7 +20,8 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "freescale/aux_bases_lemmas.ma".
+include "freescale/oct_lemmas.ma".
+include "freescale/bitrigesim_lemmas.ma".
 include "freescale/exadecim_lemmas.ma".
 include "freescale/opcode_base.ma".
 
@@ -35,11 +36,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 +53,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 +70,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 +87,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 +104,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 +121,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 +138,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 +155,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 +172,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 +189,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 +206,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 +223,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 +240,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 +257,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 +274,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 +291,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 +308,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 +325,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 +342,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 +359,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 +376,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 +393,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 +410,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 +427,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 +444,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 +461,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 +478,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 +495,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 +512,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 +529,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 +560,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 +597,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 +638,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 +687,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;