freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma
index f0954a11ccb0b57bf0cfe7f232d9937845084846..041874b6f8341f964fbc853b0e5a9ad8b3d4a712 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma
@@ -30,7 +30,7 @@ include "freescale/opcode_base.ma".
 ndefinition opcode_destruct1 : Πop2.ΠP:Prop.ADC = op2 → match op2 with [ ADC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##1: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ADC with [ ADC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -39,7 +39,7 @@ nqed.
 ndefinition opcode_destruct2 : Πop2.ΠP:Prop.ADD = op2 → match op2 with [ ADD ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##2: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ADD with [ ADD ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -48,7 +48,7 @@ nqed.
 ndefinition opcode_destruct3 : Πop2.ΠP:Prop.AIS = op2 → match op2 with [ AIS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##3: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match AIS with [ AIS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -57,7 +57,7 @@ nqed.
 ndefinition opcode_destruct4 : Πop2.ΠP:Prop.AIX = op2 → match op2 with [ AIX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##4: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match AIX with [ AIX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -66,7 +66,7 @@ nqed.
 ndefinition opcode_destruct5 : Πop2.ΠP:Prop.AND = op2 → match op2 with [ AND ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##5: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match AND with [ AND ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -75,7 +75,7 @@ nqed.
 ndefinition opcode_destruct6 : Πop2.ΠP:Prop.ASL = op2 → match op2 with [ ASL ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##6: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ASL with [ ASL ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -84,7 +84,7 @@ nqed.
 ndefinition opcode_destruct7 : Πop2.ΠP:Prop.ASR = op2 → match op2 with [ ASR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##7: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ASR with [ ASR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -93,7 +93,7 @@ nqed.
 ndefinition opcode_destruct8 : Πop2.ΠP:Prop.BCC = op2 → match op2 with [ BCC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##8: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BCC with [ BCC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -102,7 +102,7 @@ nqed.
 ndefinition opcode_destruct9 : Πop2.ΠP:Prop.BCLRn = op2 → match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##9: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BCLRn with [ BCLRn ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -111,7 +111,7 @@ nqed.
 ndefinition opcode_destruct10 : Πop2.ΠP:Prop.BCS = op2 → match op2 with [ BCS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##10: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BCS with [ BCS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -120,7 +120,7 @@ nqed.
 ndefinition opcode_destruct11 : Πop2.ΠP:Prop.BEQ = op2 → match op2 with [ BEQ ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##11: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BEQ with [ BEQ ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -129,7 +129,7 @@ nqed.
 ndefinition opcode_destruct12 : Πop2.ΠP:Prop.BGE = op2 → match op2 with [ BGE ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##12: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BGE with [ BGE ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -138,7 +138,7 @@ nqed.
 ndefinition opcode_destruct13 : Πop2.ΠP:Prop.BGND = op2 → match op2 with [ BGND ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##13: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BGND with [ BGND ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -147,7 +147,7 @@ nqed.
 ndefinition opcode_destruct14 : Πop2.ΠP:Prop.BGT = op2 → match op2 with [ BGT ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##14: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BGT with [ BGT ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -156,7 +156,7 @@ nqed.
 ndefinition opcode_destruct15 : Πop2.ΠP:Prop.BHCC = op2 → match op2 with [ BHCC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##15: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BHCC with [ BHCC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -165,7 +165,7 @@ nqed.
 ndefinition opcode_destruct16 : Πop2.ΠP:Prop.BHCS = op2 → match op2 with [ BHCS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##16: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BHCS with [ BHCS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -174,7 +174,7 @@ nqed.
 ndefinition opcode_destruct17 : Πop2.ΠP:Prop.BHI = op2 → match op2 with [ BHI ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##17: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BHI with [ BHI ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -183,7 +183,7 @@ nqed.
 ndefinition opcode_destruct18 : Πop2.ΠP:Prop.BIH = op2 → match op2 with [ BIH ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##18: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BIH with [ BIH ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -192,7 +192,7 @@ nqed.
 ndefinition opcode_destruct19 : Πop2.ΠP:Prop.BIL = op2 → match op2 with [ BIL ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##19: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BIL with [ BIL ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -201,7 +201,7 @@ nqed.
 ndefinition opcode_destruct20 : Πop2.ΠP:Prop.BIT = op2 → match op2 with [ BIT ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##20: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BIT with [ BIT ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -210,7 +210,7 @@ nqed.
 ndefinition opcode_destruct21 : Πop2.ΠP:Prop.BLE = op2 → match op2 with [ BLE ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##21: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BLE with [ BLE ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -219,7 +219,7 @@ nqed.
 ndefinition opcode_destruct22 : Πop2.ΠP:Prop.BLS = op2 → match op2 with [ BLS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##22: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BLS with [ BLS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -228,7 +228,7 @@ nqed.
 ndefinition opcode_destruct23 : Πop2.ΠP:Prop.BLT = op2 → match op2 with [ BLT ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##23: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BLT with [ BLT ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -237,7 +237,7 @@ nqed.
 ndefinition opcode_destruct24 : Πop2.ΠP:Prop.BMC = op2 → match op2 with [ BMC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##24: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BMC with [ BMC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -246,7 +246,7 @@ nqed.
 ndefinition opcode_destruct25 : Πop2.ΠP:Prop.BMI = op2 → match op2 with [ BMI ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##25: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BMI with [ BMI ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -255,7 +255,7 @@ nqed.
 ndefinition opcode_destruct26 : Πop2.ΠP:Prop.BMS = op2 → match op2 with [ BMS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##26: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BMS with [ BMS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -264,7 +264,7 @@ nqed.
 ndefinition opcode_destruct27 : Πop2.ΠP:Prop.BNE = op2 → match op2 with [ BNE ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##27: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BNE with [ BNE ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -273,7 +273,7 @@ nqed.
 ndefinition opcode_destruct28 : Πop2.ΠP:Prop.BPL = op2 → match op2 with [ BPL ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##28: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BPL with [ BPL ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -282,7 +282,7 @@ nqed.
 ndefinition opcode_destruct29 : Πop2.ΠP:Prop.BRA = op2 → match op2 with [ BRA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##29: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BRA with [ BRA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -291,7 +291,7 @@ nqed.
 ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##30: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BRCLRn with [ BRCLRn ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -300,7 +300,7 @@ nqed.
 ndefinition opcode_destruct31 : Πop2.ΠP:Prop.BRN = op2 → match op2 with [ BRN ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##31: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BRN with [ BRN ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -309,7 +309,7 @@ nqed.
 ndefinition opcode_destruct32 : Πop2.ΠP:Prop.BRSETn = op2 → match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##32: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BRSETn with [ BRSETn ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -318,7 +318,7 @@ nqed.
 ndefinition opcode_destruct33 : Πop2.ΠP:Prop.BSETn = op2 → match op2 with [ BSETn ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##33: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BSETn with [ BSETn ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -327,7 +327,7 @@ nqed.
 ndefinition opcode_destruct34 : Πop2.ΠP:Prop.BSR = op2 → match op2 with [ BSR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##34: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match BSR with [ BSR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -336,7 +336,7 @@ nqed.
 ndefinition opcode_destruct35 : Πop2.ΠP:Prop.CBEQA = op2 → match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##35: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CBEQA with [ CBEQA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -345,7 +345,7 @@ nqed.
 ndefinition opcode_destruct36 : Πop2.ΠP:Prop.CBEQX = op2 → match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##36: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CBEQX with [ CBEQX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -354,7 +354,7 @@ nqed.
 ndefinition opcode_destruct37 : Πop2.ΠP:Prop.CLC = op2 → match op2 with [ CLC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##37: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CLC with [ CLC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -363,7 +363,7 @@ nqed.
 ndefinition opcode_destruct38 : Πop2.ΠP:Prop.CLI = op2 → match op2 with [ CLI ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##38: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CLI with [ CLI ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -372,7 +372,7 @@ nqed.
 ndefinition opcode_destruct39 : Πop2.ΠP:Prop.CLR = op2 → match op2 with [ CLR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##39: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CLR with [ CLR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -381,7 +381,7 @@ nqed.
 ndefinition opcode_destruct40 : Πop2.ΠP:Prop.CMP = op2 → match op2 with [ CMP ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##40: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CMP with [ CMP ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -390,7 +390,7 @@ nqed.
 ndefinition opcode_destruct41 : Πop2.ΠP:Prop.COM = op2 → match op2 with [ COM ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##41: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match COM with [ COM ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -399,7 +399,7 @@ nqed.
 ndefinition opcode_destruct42 : Πop2.ΠP:Prop.CPHX = op2 → match op2 with [ CPHX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##42: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CPHX with [ CPHX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -408,7 +408,7 @@ nqed.
 ndefinition opcode_destruct43 : Πop2.ΠP:Prop.CPX = op2 → match op2 with [ CPX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##43: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match CPX with [ CPX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -417,7 +417,7 @@ nqed.
 ndefinition opcode_destruct44 : Πop2.ΠP:Prop.DAA = op2 → match op2 with [ DAA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##44: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match DAA with [ DAA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -426,7 +426,7 @@ nqed.
 ndefinition opcode_destruct45 : Πop2.ΠP:Prop.DBNZ = op2 → match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##45: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match DBNZ with [ DBNZ ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -435,7 +435,7 @@ nqed.
 ndefinition opcode_destruct46 : Πop2.ΠP:Prop.DEC = op2 → match op2 with [ DEC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##46: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match DEC with [ DEC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -444,7 +444,7 @@ nqed.
 ndefinition opcode_destruct47 : Πop2.ΠP:Prop.DIV = op2 → match op2 with [ DIV ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##47: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match DIV with [ DIV ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -453,7 +453,7 @@ nqed.
 ndefinition opcode_destruct48 : Πop2.ΠP:Prop.EOR = op2 → match op2 with [ EOR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##48: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match EOR with [ EOR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -462,7 +462,7 @@ nqed.
 ndefinition opcode_destruct49 : Πop2.ΠP:Prop.INC = op2 → match op2 with [ INC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##49: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match INC with [ INC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -471,7 +471,7 @@ nqed.
 ndefinition opcode_destruct50 : Πop2.ΠP:Prop.JMP = op2 → match op2 with [ JMP ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##50: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match JMP with [ JMP ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -480,7 +480,7 @@ nqed.
 ndefinition opcode_destruct51 : Πop2.ΠP:Prop.JSR = op2 → match op2 with [ JSR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##51: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match JSR with [ JSR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -489,7 +489,7 @@ nqed.
 ndefinition opcode_destruct52 : Πop2.ΠP:Prop.LDA = op2 → match op2 with [ LDA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##52: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match LDA with [ LDA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -498,7 +498,7 @@ nqed.
 ndefinition opcode_destruct53 : Πop2.ΠP:Prop.LDHX = op2 → match op2 with [ LDHX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##53: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match LDHX with [ LDHX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -507,7 +507,7 @@ nqed.
 ndefinition opcode_destruct54 : Πop2.ΠP:Prop.LDX = op2 → match op2 with [ LDX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##54: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match LDX with [ LDX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -516,7 +516,7 @@ nqed.
 ndefinition opcode_destruct55 : Πop2.ΠP:Prop.LSR = op2 → match op2 with [ LSR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##55: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match LSR with [ LSR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -525,7 +525,7 @@ nqed.
 ndefinition opcode_destruct56 : Πop2.ΠP:Prop.MOV = op2 → match op2 with [ MOV ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##56: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match MOV with [ MOV ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -534,7 +534,7 @@ nqed.
 ndefinition opcode_destruct57 : Πop2.ΠP:Prop.MUL = op2 → match op2 with [ MUL ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##57: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match MUL with [ MUL ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -543,7 +543,7 @@ nqed.
 ndefinition opcode_destruct58 : Πop2.ΠP:Prop.NEG = op2 → match op2 with [ NEG ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##58: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match NEG with [ NEG ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -552,7 +552,7 @@ nqed.
 ndefinition opcode_destruct59 : Πop2.ΠP:Prop.NOP = op2 → match op2 with [ NOP ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##59: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match NOP with [ NOP ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -561,7 +561,7 @@ nqed.
 ndefinition opcode_destruct60 : Πop2.ΠP:Prop.NSA = op2 → match op2 with [ NSA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##60: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match NSA with [ NSA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -570,7 +570,7 @@ nqed.
 ndefinition opcode_destruct61 : Πop2.ΠP:Prop.ORA = op2 → match op2 with [ ORA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##61: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ORA with [ ORA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -579,7 +579,7 @@ nqed.
 ndefinition opcode_destruct62 : Πop2.ΠP:Prop.PSHA = op2 → match op2 with [ PSHA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##62: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match PSHA with [ PSHA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -588,7 +588,7 @@ nqed.
 ndefinition opcode_destruct63 : Πop2.ΠP:Prop.PSHH = op2 → match op2 with [ PSHH ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##63: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match PSHH with [ PSHH ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -597,7 +597,7 @@ nqed.
 ndefinition opcode_destruct64 : Πop2.ΠP:Prop.PSHX = op2 → match op2 with [ PSHX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##64: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match PSHX with [ PSHX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -606,7 +606,7 @@ nqed.
 ndefinition opcode_destruct65 : Πop2.ΠP:Prop.PULA = op2 → match op2 with [ PULA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##65: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match PULA with [ PULA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -615,7 +615,7 @@ nqed.
 ndefinition opcode_destruct66 : Πop2.ΠP:Prop.PULH = op2 → match op2 with [ PULH ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##66: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match PULH with [ PULH ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -624,7 +624,7 @@ nqed.
 ndefinition opcode_destruct67 : Πop2.ΠP:Prop.PULX = op2 → match op2 with [ PULX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##67: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match PULX with [ PULX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -633,7 +633,7 @@ nqed.
 ndefinition opcode_destruct68 : Πop2.ΠP:Prop.ROL = op2 → match op2 with [ ROL ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##68: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ROL with [ ROL ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -642,7 +642,7 @@ nqed.
 ndefinition opcode_destruct69 : Πop2.ΠP:Prop.ROR = op2 → match op2 with [ ROR ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##69: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match ROR with [ ROR ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -651,7 +651,7 @@ nqed.
 ndefinition opcode_destruct70 : Πop2.ΠP:Prop.RSP = op2 → match op2 with [ RSP ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##70: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match RSP with [ RSP ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -660,7 +660,7 @@ nqed.
 ndefinition opcode_destruct71 : Πop2.ΠP:Prop.RTI = op2 → match op2 with [ RTI ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##71: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match RTI with [ RTI ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -669,7 +669,7 @@ nqed.
 ndefinition opcode_destruct72 : Πop2.ΠP:Prop.RTS = op2 → match op2 with [ RTS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##72: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match RTS with [ RTS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -678,7 +678,7 @@ nqed.
 ndefinition opcode_destruct73 : Πop2.ΠP:Prop.SBC = op2 → match op2 with [ SBC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##73: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SBC with [ SBC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -687,7 +687,7 @@ nqed.
 ndefinition opcode_destruct74 : Πop2.ΠP:Prop.SEC = op2 → match op2 with [ SEC ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##74: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SEC with [ SEC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -696,7 +696,7 @@ nqed.
 ndefinition opcode_destruct75 : Πop2.ΠP:Prop.SEI = op2 → match op2 with [ SEI ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##75: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SEI with [ SEI ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -705,7 +705,7 @@ nqed.
 ndefinition opcode_destruct76 : Πop2.ΠP:Prop.SHA = op2 → match op2 with [ SHA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##76: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SHA with [ SHA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -714,7 +714,7 @@ nqed.
 ndefinition opcode_destruct77 : Πop2.ΠP:Prop.SLA = op2 → match op2 with [ SLA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##77: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SLA with [ SLA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -723,7 +723,7 @@ nqed.
 ndefinition opcode_destruct78 : Πop2.ΠP:Prop.STA = op2 → match op2 with [ STA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##78: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match STA with [ STA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -732,7 +732,7 @@ nqed.
 ndefinition opcode_destruct79 : Πop2.ΠP:Prop.STHX = op2 → match op2 with [ STHX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##79: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match STHX with [ STHX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -741,7 +741,7 @@ nqed.
 ndefinition opcode_destruct80 : Πop2.ΠP:Prop.STOP = op2 → match op2 with [ STOP ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##80: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match STOP with [ STOP ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -750,7 +750,7 @@ nqed.
 ndefinition opcode_destruct81 : Πop2.ΠP:Prop.STX = op2 → match op2 with [ STX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##81: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match STX with [ STX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -759,7 +759,7 @@ nqed.
 ndefinition opcode_destruct82 : Πop2.ΠP:Prop.SUB = op2 → match op2 with [ SUB ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##82: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SUB with [ SUB ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -768,7 +768,7 @@ nqed.
 ndefinition opcode_destruct83 : Πop2.ΠP:Prop.SWI = op2 → match op2 with [ SWI ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##83: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match SWI with [ SWI ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -777,7 +777,7 @@ nqed.
 ndefinition opcode_destruct84 : Πop2.ΠP:Prop.TAP = op2 → match op2 with [ TAP ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##84: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TAP with [ TAP ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -786,7 +786,7 @@ nqed.
 ndefinition opcode_destruct85 : Πop2.ΠP:Prop.TAX = op2 → match op2 with [ TAX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##85: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TAX with [ TAX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -795,7 +795,7 @@ nqed.
 ndefinition opcode_destruct86 : Πop2.ΠP:Prop.TPA = op2 → match op2 with [ TPA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##86: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TPA with [ TPA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -804,7 +804,7 @@ nqed.
 ndefinition opcode_destruct87 : Πop2.ΠP:Prop.TST = op2 → match op2 with [ TST ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##87: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TST with [ TST ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -813,7 +813,7 @@ nqed.
 ndefinition opcode_destruct88 : Πop2.ΠP:Prop.TSX = op2 → match op2 with [ TSX ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##88: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TSX with [ TSX ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -822,7 +822,7 @@ nqed.
 ndefinition opcode_destruct89 : Πop2.ΠP:Prop.TXA = op2 → match op2 with [ TXA ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##89: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TXA with [ TXA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -831,7 +831,7 @@ nqed.
 ndefinition opcode_destruct90 : Πop2.ΠP:Prop.TXS = op2 → match op2 with [ TXS ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##90: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match TXS with [ TXS ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -840,7 +840,7 @@ nqed.
 ndefinition opcode_destruct91 : Πop2.ΠP:Prop.WAIT = op2 → match op2 with [ WAIT ⇒ P → P | _ ⇒ P ].
  #op2; #P; ncases op2; nnormalize;
  ##[ ##91: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind (λ_.?) ?);
+ ##| ##*: #H; napply False_ind;
           nchange with (match WAIT with [ WAIT ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]