1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma
index e64b10cc531632c2f043a77f591848965292071f..06aa6c0401dc820c55373ff8c8b0b4e5563bbf9c 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma
@@ -29,304 +29,304 @@ include "freescale/opcode_base_lemmas_instrmode1.ma".
 nlemma symmetric_eqinstrmode : symmetricT instr_mode bool eq_instrmode.
  #i1; #i2;
  ncases i1;
- ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
+ ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  ##| ##31: ncases i2; #n1;
      ##[ ##31: #n2;
                nchange with (eq_oct n2 n1 = eq_oct n1 n2);
                nrewrite > (symmetric_eqoct n1 n2);
      ##| ##32,33,34: #n2; nnormalize 
      ##]
-     nnormalize; napply (refl_eq ??)
+     nnormalize; napply refl_eq
  ##| ##32: ncases i2; #n1;
      ##[ ##32: #n2;
                nchange with (eq_oct n2 n1 = eq_oct n1 n2);
                nrewrite > (symmetric_eqoct n1 n2);
      ##| ##31,33,34: #n2; nnormalize 
      ##]
-     nnormalize; napply (refl_eq ??)
+     nnormalize; napply refl_eq
  ##| ##33: ncases i2; #n1;
      ##[ ##33: #n2;
                nchange with (eq_ex n2 n1 = eq_ex n1 n2);
                nrewrite > (symmetric_eqex n1 n2);
      ##| ##31,32,34: #n2; nnormalize 
      ##]
-     nnormalize; napply (refl_eq ??)
+     nnormalize; napply refl_eq
  ##| ##34: ncases i2; #n1;
      ##[ ##34: #n2;
                nchange with (eq_bitrig n2 n1 = eq_bitrig n1 n2);
                nrewrite > (symmetric_eqbitrig n1 n2);
      ##| ##31,32,33: #n2; nnormalize 
      ##]
-     nnormalize; napply (refl_eq ??)
+     nnormalize; napply refl_eq
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq1 : ∀i2.eq_instrmode MODE_INH i2 = true → MODE_INH = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##1: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq2 : ∀i2.eq_instrmode MODE_INHA i2 = true → MODE_INHA = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##2: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##2: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq3 : ∀i2.eq_instrmode MODE_INHX i2 = true → MODE_INHX = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##3: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##3: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq4 : ∀i2.eq_instrmode MODE_INHH i2 = true → MODE_INHH = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##4: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##4: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq5 : ∀i2.eq_instrmode MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##5: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##5: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq6 : ∀i2.eq_instrmode MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##6: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##6: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq7 : ∀i2.eq_instrmode MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##7: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##7: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq8 : ∀i2.eq_instrmode MODE_IMM1 i2 = true → MODE_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##8: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##8: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq9 : ∀i2.eq_instrmode MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##9: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##9: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq10 : ∀i2.eq_instrmode MODE_IMM2 i2 = true → MODE_IMM2 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##10: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##10: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq11 : ∀i2.eq_instrmode MODE_DIR1 i2 = true → MODE_DIR1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##11: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##11: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq12 : ∀i2.eq_instrmode MODE_DIR2 i2 = true → MODE_DIR2 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##12: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##12: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq13 : ∀i2.eq_instrmode MODE_IX0 i2 = true → MODE_IX0 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##13: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##13: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq14 : ∀i2.eq_instrmode MODE_IX1 i2 = true → MODE_IX1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##14: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##14: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq15 : ∀i2.eq_instrmode MODE_IX2 i2 = true → MODE_IX2 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##15: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##15: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq16 : ∀i2.eq_instrmode MODE_SP1 i2 = true → MODE_SP1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##16: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##16: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq17 : ∀i2.eq_instrmode MODE_SP2 i2 = true → MODE_SP2 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##17: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##17: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq18 : ∀i2.eq_instrmode MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##18: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##18: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq19 : ∀i2.eq_instrmode MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##19: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##19: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq20 : ∀i2.eq_instrmode MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##20: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##20: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq21 : ∀i2.eq_instrmode MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##21: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##21: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq22 : ∀i2.eq_instrmode MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##22: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##22: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq23 : ∀i2.eq_instrmode MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##23: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##23: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq24 : ∀i2.eq_instrmode MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##24: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##24: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq25 : ∀i2.eq_instrmode MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##25: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##25: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq26 : ∀i2.eq_instrmode MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##26: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##26: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq27 : ∀i2.eq_instrmode MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##27: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##27: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq28 : ∀i2.eq_instrmode MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##28: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##28: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq29 : ∀i2.eq_instrmode MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##29: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##29: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
 nlemma eqinstrmode_to_eq30 : ∀i2.eq_instrmode MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
  #i2; ncases i2; nnormalize;
- ##[ ##30: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##30: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -334,10 +334,10 @@ nlemma eqinstrmode_to_eq31 : ∀n1,i2.eq_instrmode (MODE_DIRn n1) i2 = true →
  #n1; #i2; ncases i2;
  ##[ ##31: #n2; #H;
      nchange in H:(%) with (eq_oct n1 n2 = true);
-     nrewrite > (eqoct_to_eq ?? H);
-     napply (refl_eq ??)
- ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct ??? H)
- ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
+     nrewrite > (eqoct_to_eq … H);
+     napply refl_eq
+ ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
+ ##| ##*: nnormalize; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -345,10 +345,10 @@ nlemma eqinstrmode_to_eq32 : ∀n1,i2.eq_instrmode (MODE_DIRn_and_IMM1 n1) i2 =
  #n1; #i2; ncases i2;
  ##[ ##32: #n2; #H;
      nchange in H:(%) with (eq_oct n1 n2 = true);
-     nrewrite > (eqoct_to_eq ?? H);
-     napply (refl_eq ??)
- ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct ??? H)
- ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
+     nrewrite > (eqoct_to_eq … H);
+     napply refl_eq
+ ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
+ ##| ##*: nnormalize; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -356,10 +356,10 @@ nlemma eqinstrmode_to_eq33 : ∀n1,i2.eq_instrmode (MODE_TNY n1) i2 = true → M
  #n1; #i2; ncases i2;
  ##[ ##33: #n2; #H;
      nchange in H:(%) with (eq_ex n1 n2 = true);
-     nrewrite > (eqex_to_eq ?? H);
-     napply (refl_eq ??)
- ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct ??? H)
- ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
+     nrewrite > (eqex_to_eq … H);
+     napply refl_eq
+ ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
+ ##| ##*: nnormalize; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -367,10 +367,10 @@ nlemma eqinstrmode_to_eq34 : ∀n1,i2.eq_instrmode (MODE_SRT n1) i2 = true → M
  #n1; #i2; ncases i2;
  ##[ ##34: #n2; #H;
      nchange in H:(%) with (eq_bitrig n1 n2 = true);
-     nrewrite > (eqbitrig_to_eq ?? H);
-     napply (refl_eq ??)
- ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct ??? H)
- ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
+     nrewrite > (eqbitrig_to_eq … H);
+     napply refl_eq
+ ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
+ ##| ##*: nnormalize; #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -398,241 +398,241 @@ nqed.
 
 nlemma eq_to_eqinstrmode1 : ∀i2.MODE_INH = i2 → eq_instrmode MODE_INH i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##1: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##1: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode2 : ∀i2.MODE_INHA = i2 → eq_instrmode MODE_INHA i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##2: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##2: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode3 : ∀i2.MODE_INHX = i2 → eq_instrmode MODE_INHX i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##3: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##3: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode4 : ∀i2.MODE_INHH = i2 → eq_instrmode MODE_INHH i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##4: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##4: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode5 : ∀i2.MODE_INHX0ADD = i2 → eq_instrmode MODE_INHX0ADD i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##5: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##5: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode6 : ∀i2.MODE_INHX1ADD = i2 → eq_instrmode MODE_INHX1ADD i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##6: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##6: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode7 : ∀i2.MODE_INHX2ADD = i2 → eq_instrmode MODE_INHX2ADD i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##7: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##7: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode8 : ∀i2.MODE_IMM1 = i2 → eq_instrmode MODE_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##8: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##8: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode9 : ∀i2.MODE_IMM1EXT = i2 → eq_instrmode MODE_IMM1EXT i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##9: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##9: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode10 : ∀i2.MODE_IMM2 = i2 → eq_instrmode MODE_IMM2 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##10: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##10: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode11 : ∀i2.MODE_DIR1 = i2 → eq_instrmode MODE_DIR1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##11: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##11: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode12 : ∀i2.MODE_DIR2 = i2 → eq_instrmode MODE_DIR2 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##12: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##12: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode13 : ∀i2.MODE_IX0 = i2 → eq_instrmode MODE_IX0 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##13: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##13: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode14 : ∀i2.MODE_IX1 = i2 → eq_instrmode MODE_IX1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##14: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##14: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode15 : ∀i2.MODE_IX2 = i2 → eq_instrmode MODE_IX2 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##15: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##15: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode16 : ∀i2.MODE_SP1 = i2 → eq_instrmode MODE_SP1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##16: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##16: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode17 : ∀i2.MODE_SP2 = i2 → eq_instrmode MODE_SP2 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##17: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##17: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_instrmode MODE_DIR1_to_DIR1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##18: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##18: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_instrmode MODE_IMM1_to_DIR1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##19: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##19: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_instrmode MODE_IX0p_to_DIR1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##20: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##20: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_instrmode MODE_DIR1_to_IX0p i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##21: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##21: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_instrmode MODE_INHA_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##22: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##22: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_instrmode MODE_INHX_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##23: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##23: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_instrmode MODE_IMM1_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##24: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##24: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_instrmode MODE_DIR1_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##25: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##25: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_instrmode MODE_IX0_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##26: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##26: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_instrmode MODE_IX0p_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##27: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##27: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_instrmode MODE_IX1_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##28: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##28: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_instrmode MODE_IX1p_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##29: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##29: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
 nlemma eq_to_eqinstrmode30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_instrmode MODE_SP1_and_IMM1 i2 = true.
  #t2; ncases t2; nnormalize;
- ##[ ##30: #H; napply (refl_eq ??)
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; napply (instr_mode_destruct ??? H)
+ ##[ ##30: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
+ ##| ##*: #H; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
@@ -640,11 +640,11 @@ nlemma eq_to_eqinstrmode31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_instrmode (MODE_D
  #n1; #t2; ncases t2;
  ##[ ##31: #n2; #H;
      nchange with (eq_oct n1 n2 = true);
-     nrewrite > (instr_mode_destruct_MODE_DIRn ?? H);
-     nrewrite > (eq_to_eqoct n2 n2 (refl_eq ??));
-     napply (refl_eq ??)
- ##| ##32,33,34: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
+     nrewrite > (instr_mode_destruct_MODE_DIRn … H);
+     nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##32,33,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
@@ -652,11 +652,11 @@ nlemma eq_to_eqinstrmode32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_instrmod
  #n1; #t2; ncases t2;
  ##[ ##32: #n2; #H;
      nchange with (eq_oct n1 n2 = true);
-     nrewrite > (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H);
-     nrewrite > (eq_to_eqoct n2 n2 (refl_eq ??));
-     napply (refl_eq ??)
- ##| ##31,33,34: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
+     nrewrite > (instr_mode_destruct_MODE_DIRn_and_IMM1 … H);
+     nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##31,33,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
@@ -664,11 +664,11 @@ nlemma eq_to_eqinstrmode33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_instrmode (MODE_TN
  #n1; #t2; ncases t2;
  ##[ ##33: #n2; #H;
      nchange with (eq_ex n1 n2 = true);
-     nrewrite > (instr_mode_destruct_MODE_TNY ?? H);
-     nrewrite > (eq_to_eqex n2 n2 (refl_eq ??));
-     napply (refl_eq ??)
- ##| ##31,32,34: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
+     nrewrite > (instr_mode_destruct_MODE_TNY … H);
+     nrewrite > (eq_to_eqex n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##31,32,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
  ##]
 nqed.
 
@@ -676,11 +676,11 @@ nlemma eq_to_eqinstrmode34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_instrmode (MODE_SR
  #n1; #t2; ncases t2;
  ##[ ##34: #n2; #H;
      nchange with (eq_bitrig n1 n2 = true);
-     nrewrite > (instr_mode_destruct_MODE_SRT ?? H);
-     nrewrite > (eq_to_eqbitrig n2 n2 (refl_eq ??));
-     napply (refl_eq ??)
- ##| ##31,32,33: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
+     nrewrite > (instr_mode_destruct_MODE_SRT … H);
+     nrewrite > (eq_to_eqbitrig n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##31,32,33: #n; #H; nnormalize; napply (instr_mode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
  ##]
 nqed.