X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fopcode_base_lemmas_instrmode1.ma;h=2d851ffc4a0d07da35e6776e1b92250a0bca7851;hb=601baed778a190b580982b588ebe49ba3f762b30;hp=61cf6a5b86945271a6bad677e1bee1ac114e7244;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

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 61cf6a5b8..2d851ffc4 100755
--- 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
@@ -29,517 +29,7 @@ include "freescale/opcode_base.ma".
 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
 (* ********************************************** *)
 
-ndefinition instr_mode_destruct1 :
- Πi2.ΠP:Prop.MODE_INH = i2 → match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct2 :
- Πi2.ΠP:Prop.MODE_INHA = i2 → match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct3 :
- Πi2.ΠP:Prop.MODE_INHX = i2 → match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct4 :
- Πi2.ΠP:Prop.MODE_INHH = i2 → match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct5 :
- Πi2.ΠP:Prop.MODE_INHX0ADD = i2 → match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct6 :
- Πi2.ΠP:Prop.MODE_INHX1ADD = i2 → match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct7 :
- Πi2.ΠP:Prop.MODE_INHX2ADD = i2 → match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct8 :
- Πi2.ΠP:Prop.MODE_IMM1 = i2 → match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct9 :
- Πi2.ΠP:Prop.MODE_IMM1EXT = i2 → match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct10 :
- Πi2.ΠP:Prop.MODE_IMM2 = i2 → match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct11 :
- Πi2.ΠP:Prop.MODE_DIR1 = i2 → match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct12 :
- Πi2.ΠP:Prop.MODE_DIR2 = i2 → match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct13 :
- Πi2.ΠP:Prop.MODE_IX0 = i2 → match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct14 :
- Πi2.ΠP:Prop.MODE_IX1 = i2 → match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct15 :
- Πi2.ΠP:Prop.MODE_IX2 = i2 → match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct16 :
- Πi2.ΠP:Prop.MODE_SP1 = i2 → match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct17 :
- Πi2.ΠP:Prop.MODE_SP2 = i2 → match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
-     napply False_ind;
-     nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct18 :
- Πi2.ΠP:Prop.MODE_DIR1_to_DIR1 = i2 → match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct19 :
- Πi2.ΠP:Prop.MODE_IMM1_to_DIR1 = i2 → match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct20 :
- Πi2.ΠP:Prop.MODE_IX0p_to_DIR1 = i2 → match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct21 :
- Πi2.ΠP:Prop.MODE_DIR1_to_IX0p = i2 → match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct22 :
- Πi2.ΠP:Prop.MODE_INHA_and_IMM1 = i2 → match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct23 :
- Πi2.ΠP:Prop.MODE_INHX_and_IMM1 = i2 → match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct24 :
- Πi2.ΠP:Prop.MODE_IMM1_and_IMM1 = i2 → match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct25 :
- Πi2.ΠP:Prop.MODE_DIR1_and_IMM1 = i2 → match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct26 :
- Πi2.ΠP:Prop.MODE_IX0_and_IMM1 = i2 → match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct27 :
- Πi2.ΠP:Prop.MODE_IX0p_and_IMM1 = i2 → match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct28 :
- Πi2.ΠP:Prop.MODE_IX1_and_IMM1 = i2 → match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct29 :
- Πi2.ΠP:Prop.MODE_IX1p_and_IMM1 = i2 → match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct30 :
- Πi2.ΠP:Prop.MODE_SP1_and_IMM1 = i2 → match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
-     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;
-     nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
+nlemma instrmode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
  #n1; #n2; #H;
  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
@@ -547,36 +37,7 @@ nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 →
  napply refl_eq.
 nqed.
 
-ndefinition instr_mode_destruct31 :
- Πn1,i2.ΠP:Prop.MODE_DIRn n1 = i2 →
-  match i2 with
-   [ MODE_DIRn n2 ⇒ match n1 with
-    [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
-    | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
-    | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
-    | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ].
- #n1; #i2; #P;
- 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;
-     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;
-     nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##31: #n2;
-     ncases n1;
-     ncases n2;
-     nnormalize;
-     ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn … H))
-     ##]
-nqed.
-
-nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
+nlemma instrmode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
  #n1; #n2; #H;
  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
@@ -584,347 +45,711 @@ nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 =
  napply refl_eq.
 nqed.
 
-ndefinition instr_mode_destruct32 :
- Πn1,i2.ΠP:Prop.MODE_DIRn_and_IMM1 n1 = i2 →
-  match i2 with
-   [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
-    [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
-    | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
-    | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
-    | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ].
- #n1; #i2; #P;
- ncases i2;
+nlemma instrmode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
+ #e1; #e2; #H;
+ nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
+ nrewrite < H;
  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;
-     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;
-     nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##32: #n2;
-     ncases n1;
-     ncases n2;
-     nnormalize;
-     ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn_and_IMM1 … H))
-     ##]
+ napply refl_eq.
 nqed.
 
-nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1 = n2.
- #n1; #n2; #H;
- nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
+nlemma instrmode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
+ #t1; #t2; #H;
+ nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
  napply refl_eq.
 nqed.
 
-ndefinition instr_mode_destruct33 :
- Πn1,i2.ΠP:Prop.MODE_TNY n1 = i2 →
-  match i2 with
-   [ MODE_TNY n2 ⇒ match n1 with
-    [ x0 ⇒ match n2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match n2 with [ x1 ⇒ P → P | _ ⇒ P ]
-    | x2 ⇒ match n2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match n2 with [ x3 ⇒ P → P | _ ⇒ P ]
-    | x4 ⇒ match n2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match n2 with [ x5 ⇒ P → P | _ ⇒ P ]
-    | x6 ⇒ match n2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match n2 with [ x7 ⇒ P → P | _ ⇒ P ]
-    | x8 ⇒ match n2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match n2 with [ x9 ⇒ P → P | _ ⇒ P ]
-    | xA ⇒ match n2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match n2 with [ xB ⇒ P → P | _ ⇒ P ]
-    | xC ⇒ match n2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match n2 with [ xD ⇒ P → P | _ ⇒ P ]
-    | xE ⇒ match n2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match n2 with [ xF ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ].
- #n1; #i2; #P;
- 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;
-     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;
-     nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##33: #n2;
-     ncases n1;
-     ncases n2;
-     nnormalize;
-     ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (exadecim_destruct … (instr_mode_destruct_MODE_TNY … H))
+ndefinition instrmode_destruct_aux ≝
+Πi1,i2.ΠP:Prop.i1 = i2 →
+ match eq_im i1 i2 with [ true ⇒ P → P | false ⇒ P ].
+
+ndefinition instrmode_destruct : instrmode_destruct_aux.
+ #t1; #t2; #P; #H;
+ nrewrite < H;
+ nelim t1;
+ nnormalize;
+ ##[ ##31,32,33,34: #sub; nelim sub; nnormalize ##]
+ napply (λx.x).
+nqed.
+
+nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
+ #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
+ ##| ##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
+ ##| ##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
+ ##| ##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
+ ##| ##34: ncases i2; #n1;
+     ##[ ##34: #n2;
+               nchange with (eq_bit n2 n1 = eq_bit n1 n2);
+               nrewrite > (symmetric_eqbit n1 n2);
+     ##| ##31,32,33: #n2; nnormalize 
+     ##]
+     nnormalize; napply refl_eq
+ ##]
 nqed.
 
-nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1 = n2.
- #n1; #n2; #H;
- nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
+nlemma eqim_to_eq1 : ∀i2.eq_im 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)
+ ##]
 nqed.
 
-ndefinition instr_mode_destruct34 :
- Πn1,i2.ΠP:Prop.MODE_SRT n1 = i2 →
-  match i2 with
-   [ MODE_SRT n2 ⇒ match n1 with
-    [ t00 ⇒ match n2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match n2 with [ t01 ⇒ P → P | _ ⇒ P ]
-    | t02 ⇒ match n2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match n2 with [ t03 ⇒ P → P | _ ⇒ P ]
-    | t04 ⇒ match n2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match n2 with [ t05 ⇒ P → P | _ ⇒ P ]
-    | t06 ⇒ match n2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match n2 with [ t07 ⇒ P → P | _ ⇒ P ]
-    | t08 ⇒ match n2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match n2 with [ t09 ⇒ P → P | _ ⇒ P ]
-    | t0A ⇒ match n2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match n2 with [ t0B ⇒ P → P | _ ⇒ P ]
-    | t0C ⇒ match n2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match n2 with [ t0D ⇒ P → P | _ ⇒ P ]
-    | t0E ⇒ match n2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match n2 with [ t0F ⇒ P → P | _ ⇒ P ]
-    | t10 ⇒ match n2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match n2 with [ t11 ⇒ P → P | _ ⇒ P ]
-    | t12 ⇒ match n2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match n2 with [ t13 ⇒ P → P | _ ⇒ P ]
-    | t14 ⇒ match n2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match n2 with [ t15 ⇒ P → P | _ ⇒ P ]
-    | t16 ⇒ match n2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match n2 with [ t17 ⇒ P → P | _ ⇒ P ]
-    | t18 ⇒ match n2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match n2 with [ t19 ⇒ P → P | _ ⇒ P ]
-    | t1A ⇒ match n2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match n2 with [ t1B ⇒ P → P | _ ⇒ P ]
-    | t1C ⇒ match n2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match n2 with [ t1D ⇒ P → P | _ ⇒ P ]
-    | t1E ⇒ match n2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match n2 with [ t1F ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ].
- #n1; #i2; #P;
- 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;
-     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;
-     nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
-     nrewrite > H; nnormalize; napply I
- ##| ##34: #n2;
-     ncases n1;
-     ##[ ##1: ncases n2; nnormalize;
-              ##[ ##1: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##2: ncases n2; nnormalize;
-              ##[ ##2: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##3: ncases n2; nnormalize;
-              ##[ ##3: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##4: ncases n2; nnormalize;
-              ##[ ##4: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##5: ncases n2; nnormalize;
-              ##[ ##5: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##6: ncases n2; nnormalize;
-              ##[ ##6: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##7: ncases n2; nnormalize;
-              ##[ ##7: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##8: ncases n2; nnormalize;
-              ##[ ##8: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##9: ncases n2; nnormalize;
-              ##[ ##9: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##10: ncases n2; nnormalize;
-              ##[ ##10: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##11: ncases n2; nnormalize;
-              ##[ ##11: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##12: ncases n2; nnormalize;
-              ##[ ##12: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##13: ncases n2; nnormalize;
-              ##[ ##13: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##14: ncases n2; nnormalize;
-              ##[ ##14: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##15: ncases n2; nnormalize;
-              ##[ ##15: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##16: ncases n2; nnormalize;
-              ##[ ##16: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##17: ncases n2; nnormalize;
-              ##[ ##17: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##18: ncases n2; nnormalize;
-              ##[ ##18: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##19: ncases n2; nnormalize;
-              ##[ ##19: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##20: ncases n2; nnormalize;
-              ##[ ##20: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##21: ncases n2; nnormalize;
-              ##[ ##21: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##22: ncases n2; nnormalize;
-              ##[ ##22: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##23: ncases n2; nnormalize;
-              ##[ ##23: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##24: ncases n2; nnormalize;
-              ##[ ##24: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##25: ncases n2; nnormalize;
-              ##[ ##25: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##26: ncases n2; nnormalize;
-              ##[ ##26: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##27: ncases n2; nnormalize;
-              ##[ ##27: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##28: ncases n2; nnormalize;
-              ##[ ##28: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##29: ncases n2; nnormalize;
-              ##[ ##29: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##30: ncases n2; nnormalize;
-              ##[ ##30: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##31: ncases n2; nnormalize;
-              ##[ ##31: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##| ##32: ncases n2; nnormalize;
-              ##[ ##32: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
-              ##]
-     ##]
+nlemma eqim_to_eq2 : ∀i2.eq_im 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)
  ##]
 nqed.
 
-ndefinition instr_mode_destruct_aux ≝
-Πi1,i2.ΠP:Prop.i1 = i2 →
- match i1 with
-  [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ]
-  | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ]
-  | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ]
-  | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ]
-  | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ]
-  | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ]
-  | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ]
-  | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ]
-  | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ]
-  | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ]
-  | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ]
-  | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ]
-  | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ]
-  | MODE_DIR1_to_DIR1  ⇒ match i2 with [ MODE_DIR1_to_DIR1  ⇒ P → P | _ ⇒ P ]
-  | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ]
-  | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ]
-  | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ]
-  | MODE_DIRn n1 ⇒ match i2 with
-   [ MODE_DIRn n2 ⇒ match n1 with
-    [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
-    | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
-    | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
-    | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ]
-  | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with
-   [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
-    [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ] 
-    | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
-    | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
-    | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ]
-  | MODE_TNY e1 ⇒ match i2 with
-   [ MODE_TNY e2 ⇒ match e1 with
-    [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
-    | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
-    | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
-    | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
-    | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
-    | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
-    | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
-    | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]]
-   | _ ⇒ P ]
-  | MODE_SRT t1 ⇒ match i2 with
-   [ MODE_SRT t2 ⇒ match t1 with
-    [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
-    | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
-    | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
-    | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
-    | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
-    | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
-    | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
-    | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
-    | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
-    | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
-    | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
-    | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
-    | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
-    | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
-    | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
-    | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]]
-    | _ ⇒ P ]
-  ].
-
-ndefinition instr_mode_destruct : instr_mode_destruct_aux.
- #t1; ncases t1;
- ##[ ##1: napply instr_mode_destruct1 ##| ##2: napply instr_mode_destruct2
- ##| ##3: napply instr_mode_destruct3 ##| ##4: napply instr_mode_destruct4
- ##| ##5: napply instr_mode_destruct5 ##| ##6: napply instr_mode_destruct6
- ##| ##7: napply instr_mode_destruct7 ##| ##8: napply instr_mode_destruct8
- ##| ##9: napply instr_mode_destruct9 ##| ##10: napply instr_mode_destruct10
- ##| ##11: napply instr_mode_destruct11 ##| ##12: napply instr_mode_destruct12
- ##| ##13: napply instr_mode_destruct13 ##| ##14: napply instr_mode_destruct14
- ##| ##15: napply instr_mode_destruct15 ##| ##16: napply instr_mode_destruct16
- ##| ##17: napply instr_mode_destruct17 ##| ##18: napply instr_mode_destruct18
- ##| ##19: napply instr_mode_destruct19 ##| ##20: napply instr_mode_destruct20
- ##| ##21: napply instr_mode_destruct21 ##| ##22: napply instr_mode_destruct22
- ##| ##23: napply instr_mode_destruct23 ##| ##24: napply instr_mode_destruct24
- ##| ##25: napply instr_mode_destruct25 ##| ##26: napply instr_mode_destruct26
- ##| ##27: napply instr_mode_destruct27 ##| ##28: napply instr_mode_destruct28
- ##| ##29: napply instr_mode_destruct29 ##| ##30: napply instr_mode_destruct30
- ##| ##31: napply instr_mode_destruct31 ##| ##32: napply instr_mode_destruct32
- ##| ##33: napply instr_mode_destruct33 ##| ##34: napply instr_mode_destruct34
+nlemma eqim_to_eq3 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq4 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq5 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq6 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq7 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq8 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq9 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq10 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq11 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq12 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq13 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq14 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq15 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq16 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq17 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq18 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq19 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq20 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq21 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq22 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq23 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq24 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq25 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq26 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq27 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq28 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq29 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq30 : ∀i2.eq_im 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
+ #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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → 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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
+ #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)
+ ##]
+nqed.
+
+nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
+ #n1; #i2; ncases i2;
+ ##[ ##34: #n2; #H;
+     nchange in H:(%) with (eq_bit n1 n2 = true);
+     nrewrite > (eqbit_to_eq … H);
+     napply refl_eq
+ ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
+ ##| ##*: nnormalize; #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
+ #i1; ncases i1;
+ ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
+ ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
+ ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
+ ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
+ ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
+ ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
+ ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
+ ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
+ ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
+ ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
+ ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
+ ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
+ ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
+ ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
+ ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
+ ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
+ ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
+ ##]
+nqed.
+
+nlemma eq_to_eqim1 : ∀i2.MODE_INH = i2 → eq_im MODE_INH i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##1: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim2 : ∀i2.MODE_INHA = i2 → eq_im MODE_INHA i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##2: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim3 : ∀i2.MODE_INHX = i2 → eq_im MODE_INHX i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##3: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim4 : ∀i2.MODE_INHH = i2 → eq_im MODE_INHH i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##4: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim5 : ∀i2.MODE_INHX0ADD = i2 → eq_im MODE_INHX0ADD i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##5: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim6 : ∀i2.MODE_INHX1ADD = i2 → eq_im MODE_INHX1ADD i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##6: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim7 : ∀i2.MODE_INHX2ADD = i2 → eq_im MODE_INHX2ADD i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##7: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim8 : ∀i2.MODE_IMM1 = i2 → eq_im MODE_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##8: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim9 : ∀i2.MODE_IMM1EXT = i2 → eq_im MODE_IMM1EXT i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##9: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim10 : ∀i2.MODE_IMM2 = i2 → eq_im MODE_IMM2 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##10: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim11 : ∀i2.MODE_DIR1 = i2 → eq_im MODE_DIR1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##11: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim12 : ∀i2.MODE_DIR2 = i2 → eq_im MODE_DIR2 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##12: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim13 : ∀i2.MODE_IX0 = i2 → eq_im MODE_IX0 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##13: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim14 : ∀i2.MODE_IX1 = i2 → eq_im MODE_IX1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##14: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim15 : ∀i2.MODE_IX2 = i2 → eq_im MODE_IX2 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##15: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim16 : ∀i2.MODE_SP1 = i2 → eq_im MODE_SP1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##16: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim17 : ∀i2.MODE_SP2 = i2 → eq_im MODE_SP2 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##17: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_im MODE_DIR1_to_DIR1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##18: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_im MODE_IMM1_to_DIR1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##19: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_im MODE_IX0p_to_DIR1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##20: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_im MODE_DIR1_to_IX0p i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##21: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_im MODE_INHA_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##22: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_im MODE_INHX_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##23: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_im MODE_IMM1_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##24: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_im MODE_DIR1_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##25: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_im MODE_IX0_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##26: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_im MODE_IX0p_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##27: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_im MODE_IX1_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##28: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_im MODE_IX1p_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##29: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_im MODE_SP1_and_IMM1 i2 = true.
+ #t2; ncases t2; nnormalize;
+ ##[ ##30: #H; napply refl_eq
+ ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
+ ##| ##*: #H; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_im (MODE_DIRn n1) i2 = true.
+ #n1; #t2; ncases t2;
+ ##[ ##31: #n2; #H;
+     nchange with (eq_oct n1 n2 = true);
+     nrewrite > (instrmode_destruct_MODE_DIRn n1 n2 H);
+     nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##32,33,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_im (MODE_DIRn_and_IMM1 n1) i2 = true.
+ #n1; #t2; ncases t2;
+ ##[ ##32: #n2; #H;
+     nchange with (eq_oct n1 n2 = true);
+     nrewrite > (instrmode_destruct_MODE_DIRn_and_IMM1 … H);
+     nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##31,33,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_im (MODE_TNY n1) i2 = true.
+ #n1; #t2; ncases t2;
+ ##[ ##33: #n2; #H;
+     nchange with (eq_ex n1 n2 = true);
+     nrewrite > (instrmode_destruct_MODE_TNY … H);
+     nrewrite > (eq_to_eqex n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##31,32,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_im (MODE_SRT n1) i2 = true.
+ #n1; #t2; ncases t2;
+ ##[ ##34: #n2; #H;
+     nchange with (eq_bit n1 n2 = true);
+     nrewrite > (instrmode_destruct_MODE_SRT … H);
+     nrewrite > (eq_to_eqbit n2 n2 (refl_eq …));
+     napply refl_eq
+ ##| ##31,32,33: #n; #H; nnormalize; napply (instrmode_destruct … H)
+ ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqim : ∀i1,i2.i1 = i2 → eq_im i1 i2 = true.
+ #i1; ncases i1;
+ ##[ ##1: napply eq_to_eqim1 ##| ##2: napply eq_to_eqim2
+ ##| ##3: napply eq_to_eqim3 ##| ##4: napply eq_to_eqim4
+ ##| ##5: napply eq_to_eqim5 ##| ##6: napply eq_to_eqim6
+ ##| ##7: napply eq_to_eqim7 ##| ##8: napply eq_to_eqim8
+ ##| ##9: napply eq_to_eqim9 ##| ##10: napply eq_to_eqim10 
+ ##| ##11: napply eq_to_eqim11 ##| ##12: napply eq_to_eqim12
+ ##| ##13: napply eq_to_eqim13 ##| ##14: napply eq_to_eqim14
+ ##| ##15: napply eq_to_eqim15 ##| ##16: napply eq_to_eqim16
+ ##| ##17: napply eq_to_eqim17 ##| ##18: napply eq_to_eqim18
+ ##| ##19: napply eq_to_eqim19 ##| ##20: napply eq_to_eqim20
+ ##| ##21: napply eq_to_eqim21 ##| ##22: napply eq_to_eqim22
+ ##| ##23: napply eq_to_eqim23 ##| ##24: napply eq_to_eqim24
+ ##| ##25: napply eq_to_eqim25 ##| ##26: napply eq_to_eqim26
+ ##| ##27: napply eq_to_eqim27 ##| ##28: napply eq_to_eqim28
+ ##| ##29: napply eq_to_eqim29 ##| ##30: napply eq_to_eqim30
+ ##| ##31: napply eq_to_eqim31 ##| ##32: napply eq_to_eqim32
+ ##| ##33: napply eq_to_eqim33 ##| ##34: napply eq_to_eqim34
  ##]
 nqed.