X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Faux_bases_lemmas.ma;h=0cc21054beef29aef7a67e490833f1dfb90501ad;hb=20fdd66303330e6209059e90b6a98af71ec29567;hp=55ef3df2367d79e1a56441ff9899ea087eec39be;hpb=661cf1186c81c15122e0644b679795d2e6b9d389;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
index 55ef3df23..0cc21054b 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
@@ -31,8 +31,8 @@ include "freescale/aux_bases.ma".
 (* OTTALI *)
 (* ****** *)
 
-ndefinition oct_destruct :
- Πn1,n2:oct.ΠP:Prop.n1 = n2 →
+ndefinition oct_destruct_aux ≝
+Πn1,n2:oct.ΠP:Prop.n1 = n2 →
  match n1 with
   [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
   | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
@@ -43,6 +43,8 @@ ndefinition oct_destruct :
   | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
   | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
   ].
+
+ndefinition oct_destruct : oct_destruct_aux.
  #n1; #n2; #P;
  nelim n1;
  ##[ ##1: nelim n2; nnormalize; #H;
@@ -128,8 +130,392 @@ nqed.
 (* BITRIGESIMALI *)
 (* ************* *)
 
-ndefinition bitrigesim_destruct :
- Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
+ndefinition bitrigesim_destruct1 :
+Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct2 :
+Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct3 :
+Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct4 :
+Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct5 :
+Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct6 :
+Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct7 :
+Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct8 :
+Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct9 :
+Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##9: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct10 :
+Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##10: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct11 :
+Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##11: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct12 :
+Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##12: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct13 :
+Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##13: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct14 :
+Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##14: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct15 :
+Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##15: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct16 :
+Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##16: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct17 :
+Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##17: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct18 :
+Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##18: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct19 :
+Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##19: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct20 :
+Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##20: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct21 :
+Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##21: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct22 :
+Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##22: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct23 :
+Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##23: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct24 :
+Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##24: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct25 :
+Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##25: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct26 :
+Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##26: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct27 :
+Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##27: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct28 :
+Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##28: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct29 :
+Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##29: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct30 :
+Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##30: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct31 :
+Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##31: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct32 :
+Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##32: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct_aux ≝
+Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
  match t1 with
   [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
   | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
@@ -164,202 +550,44 @@ ndefinition bitrigesim_destruct :
   | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
   | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
   ].
- #t1; #t2; #P;
- nelim t1;
- ##[ ##1: nelim t2; nnormalize; #H;
-          ##[ ##1: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##2: nelim t2; nnormalize; #H;
-          ##[ ##2: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##3: nelim t2; nnormalize; #H;
-          ##[ ##3: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##4: nelim t2; nnormalize; #H;
-          ##[ ##4: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##5: nelim t2; nnormalize; #H;
-          ##[ ##5: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##6: nelim t2; nnormalize; #H;
-          ##[ ##6: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##7: nelim t2; nnormalize; #H;
-          ##[ ##7: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##8: nelim t2; nnormalize; #H;
-          ##[ ##8: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##9: nelim t2; nnormalize; #H;
-          ##[ ##9: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##10: nelim t2; nnormalize; #H;
-          ##[ ##10: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##11: nelim t2; nnormalize; #H;
-          ##[ ##11: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##12: nelim t2; nnormalize; #H;
-          ##[ ##12: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##13: nelim t2; nnormalize; #H;
-          ##[ ##13: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##14: nelim t2; nnormalize; #H;
-          ##[ ##14: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##15: nelim t2; nnormalize; #H;
-          ##[ ##15: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##16: nelim t2; nnormalize; #H;
-          ##[ ##16: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##17: nelim t2; nnormalize; #H;
-          ##[ ##17: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##18: nelim t2; nnormalize; #H;
-          ##[ ##18: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##19: nelim t2; nnormalize; #H;
-          ##[ ##19: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##20: nelim t2; nnormalize; #H;
-          ##[ ##20: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##21: nelim t2; nnormalize; #H;
-          ##[ ##21: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##22: nelim t2; nnormalize; #H;
-          ##[ ##22: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##23: nelim t2; nnormalize; #H;
-          ##[ ##23: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##24: nelim t2; nnormalize; #H;
-          ##[ ##24: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##25: nelim t2; nnormalize; #H;
-          ##[ ##25: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##26: nelim t2; nnormalize; #H;
-          ##[ ##26: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##27: nelim t2; nnormalize; #H;
-          ##[ ##27: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##28: nelim t2; nnormalize; #H;
-          ##[ ##28: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##29: nelim t2; nnormalize; #H;
-          ##[ ##29: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##30: nelim t2; nnormalize; #H;
-          ##[ ##30: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##31: nelim t2; nnormalize; #H;
-          ##[ ##31: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##32: nelim t2; nnormalize; #H;
-          ##[ ##32: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
+
+ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
+ #t1;
+ ncases t1;
+ ##[ ##1: napply bitrigesim_destruct1
+ ##| ##2: napply bitrigesim_destruct2
+ ##| ##3: napply bitrigesim_destruct3
+ ##| ##4: napply bitrigesim_destruct4
+ ##| ##5: napply bitrigesim_destruct5
+ ##| ##6: napply bitrigesim_destruct6
+ ##| ##7: napply bitrigesim_destruct7
+ ##| ##8: napply bitrigesim_destruct8
+ ##| ##9: napply bitrigesim_destruct9
+ ##| ##10: napply bitrigesim_destruct10
+ ##| ##11: napply bitrigesim_destruct11
+ ##| ##12: napply bitrigesim_destruct12
+ ##| ##13: napply bitrigesim_destruct13
+ ##| ##14: napply bitrigesim_destruct14
+ ##| ##15: napply bitrigesim_destruct15
+ ##| ##16: napply bitrigesim_destruct16
+ ##| ##17: napply bitrigesim_destruct17
+ ##| ##18: napply bitrigesim_destruct18
+ ##| ##19: napply bitrigesim_destruct19
+ ##| ##20: napply bitrigesim_destruct20
+ ##| ##21: napply bitrigesim_destruct21
+ ##| ##22: napply bitrigesim_destruct22
+ ##| ##23: napply bitrigesim_destruct23
+ ##| ##24: napply bitrigesim_destruct24
+ ##| ##25: napply bitrigesim_destruct25
+ ##| ##26: napply bitrigesim_destruct26
+ ##| ##27: napply bitrigesim_destruct27
+ ##| ##28: napply bitrigesim_destruct28
+ ##| ##29: napply bitrigesim_destruct29
+ ##| ##30: napply bitrigesim_destruct30
+ ##| ##31: napply bitrigesim_destruct31
+ ##| ##32: napply bitrigesim_destruct32
  ##]
-nqed.
+nqed. 
 
 nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
  #t1;
@@ -399,270 +627,333 @@ nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
  ##]
 nqed.
 
+nlemma eqbitrig_to_eq1 : ∀t2.eq_bitrig t00 t2 = true → t00 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq2 : ∀t2.eq_bitrig t01 t2 = true → t01 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq3 : ∀t2.eq_bitrig t02 t2 = true → t02 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq4 : ∀t2.eq_bitrig t03 t2 = true → t03 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq5 : ∀t2.eq_bitrig t04 t2 = true → t04 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq6 : ∀t2.eq_bitrig t05 t2 = true → t05 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq7 : ∀t2.eq_bitrig t06 t2 = true → t06 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq8 : ∀t2.eq_bitrig t07 t2 = true → t07 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq9 : ∀t2.eq_bitrig t08 t2 = true → t08 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq10 : ∀t2.eq_bitrig t09 t2 = true → t09 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq11 : ∀t2.eq_bitrig t0A t2 = true → t0A = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq12 : ∀t2.eq_bitrig t0B t2 = true → t0B = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq13 : ∀t2.eq_bitrig t0C t2 = true → t0C = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq14 : ∀t2.eq_bitrig t0D t2 = true → t0D = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq15 : ∀t2.eq_bitrig t0E t2 = true → t0E = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq16 : ∀t2.eq_bitrig t0F t2 = true → t0F = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq17 : ∀t2.eq_bitrig t10 t2 = true → t10 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq18 : ∀t2.eq_bitrig t11 t2 = true → t11 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq19 : ∀t2.eq_bitrig t12 t2 = true → t12 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq20 : ∀t2.eq_bitrig t13 t2 = true → t13 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq21 : ∀t2.eq_bitrig t14 t2 = true → t14 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq22 : ∀t2.eq_bitrig t15 t2 = true → t15 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq23 : ∀t2.eq_bitrig t16 t2 = true → t16 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq24 : ∀t2.eq_bitrig t17 t2 = true → t17 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq25 : ∀t2.eq_bitrig t18 t2 = true → t18 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq26 : ∀t2.eq_bitrig t19 t2 = true → t19 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq27 : ∀t2.eq_bitrig t1A t2 = true → t1A = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq28 : ∀t2.eq_bitrig t1B t2 = true → t1B = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq29 : ∀t2.eq_bitrig t1C t2 = true → t1C = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq30 : ∀t2.eq_bitrig t1D t2 = true → t1D = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq31 : ∀t2.eq_bitrig t1E t2 = true → t1E = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
+nlemma eqbitrig_to_eq32 : ∀t2.eq_bitrig t1F t2 = true → t1F = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+nqed.
+
 nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
- #t1; #t2;
+ #t1;
  ncases t1;
- ##[ ##1: ncases t2; nnormalize; #H;
-          ##[ ##1: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##2: ncases t2; nnormalize; #H;
-          ##[ ##2: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]          
- ##| ##3: ncases t2; nnormalize; #H;
-          ##[ ##3: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##4: ncases t2; nnormalize; #H;
-          ##[ ##4: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##5: ncases t2; nnormalize; #H;
-          ##[ ##5: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##6: ncases t2; nnormalize; #H;
-          ##[ ##6: napply (refl_eq ??)
-          ##| ##*:napply (bool_destruct ??? H)
-          ##]
- ##| ##7: ncases t2; nnormalize; #H;
-          ##[ ##7: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##8: ncases t2; nnormalize; #H;
-          ##[ ##8: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##9: ncases t2; nnormalize; #H;
-          ##[ ##9: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##10: ncases t2; nnormalize; #H;
-          ##[ ##10: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##11: ncases t2; nnormalize; #H;
-          ##[ ##11: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]            
- ##| ##12: ncases t2; nnormalize; #H;
-          ##[ ##12: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##13: ncases t2; nnormalize; #H;
-          ##[ ##13: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##14: ncases t2; nnormalize; #H;
-          ##[ ##14: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##15: ncases t2; nnormalize; #H;
-          ##[ ##15: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]            
- ##| ##16: ncases t2; nnormalize; #H;
-          ##[ ##16: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##17: ncases t2; nnormalize; #H;
-          ##[ ##17: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##18: ncases t2; nnormalize; #H;
-          ##[ ##18: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##19: ncases t2; nnormalize; #H;
-          ##[ ##19: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]            
- ##| ##20: ncases t2; nnormalize; #H;
-          ##[ ##20: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##21: ncases t2; nnormalize; #H;
-          ##[ ##21: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##22: ncases t2; nnormalize; #H;
-          ##[ ##22: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##23: ncases t2; nnormalize; #H;
-          ##[ ##23: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##24: ncases t2; nnormalize; #H;
-          ##[ ##24: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##25: ncases t2; nnormalize; #H;
-          ##[ ##25: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##26: ncases t2; nnormalize; #H;
-          ##[ ##26: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##27: ncases t2; nnormalize; #H;
-          ##[ ##27: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##28: ncases t2; nnormalize; #H;
-          ##[ ##28: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##29: ncases t2; nnormalize; #H;
-          ##[ ##29: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##30: ncases t2; nnormalize; #H;
-          ##[ ##30: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##31: ncases t2; nnormalize; #H;
-          ##[ ##31: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
- ##| ##32: ncases t2; nnormalize; #H;
-          ##[ ##32: napply (refl_eq ??)
-          ##| ##*: napply (bool_destruct ??? H)
-          ##]
+ ##[ ##1: napply eqbitrig_to_eq1
+ ##| ##2: napply eqbitrig_to_eq2
+ ##| ##3: napply eqbitrig_to_eq3
+ ##| ##4: napply eqbitrig_to_eq4
+ ##| ##5: napply eqbitrig_to_eq5
+ ##| ##6: napply eqbitrig_to_eq6
+ ##| ##7: napply eqbitrig_to_eq7
+ ##| ##8: napply eqbitrig_to_eq8
+ ##| ##9: napply eqbitrig_to_eq9
+ ##| ##10: napply eqbitrig_to_eq10
+ ##| ##11: napply eqbitrig_to_eq11
+ ##| ##12: napply eqbitrig_to_eq12
+ ##| ##13: napply eqbitrig_to_eq13
+ ##| ##14: napply eqbitrig_to_eq14
+ ##| ##15: napply eqbitrig_to_eq15
+ ##| ##16: napply eqbitrig_to_eq16
+ ##| ##17: napply eqbitrig_to_eq17
+ ##| ##18: napply eqbitrig_to_eq18
+ ##| ##19: napply eqbitrig_to_eq19
+ ##| ##20: napply eqbitrig_to_eq20
+ ##| ##21: napply eqbitrig_to_eq21
+ ##| ##22: napply eqbitrig_to_eq22
+ ##| ##23: napply eqbitrig_to_eq23
+ ##| ##24: napply eqbitrig_to_eq24
+ ##| ##25: napply eqbitrig_to_eq25
+ ##| ##26: napply eqbitrig_to_eq26
+ ##| ##27: napply eqbitrig_to_eq27
+ ##| ##28: napply eqbitrig_to_eq28
+ ##| ##29: napply eqbitrig_to_eq29
+ ##| ##30: napply eqbitrig_to_eq30
+ ##| ##31: napply eqbitrig_to_eq31
+ ##| ##32: napply eqbitrig_to_eq32
  ##]
 nqed.
 
+nlemma eq_to_eqbitrig1 : ∀t2.t00 = t2 → eq_bitrig t00 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig2 : ∀t2.t01 = t2 → eq_bitrig t01 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig3 : ∀t2.t02 = t2 → eq_bitrig t02 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig4 : ∀t2.t03 = t2 → eq_bitrig t03 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig5 : ∀t2.t04 = t2 → eq_bitrig t04 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig6 : ∀t2.t05 = t2 → eq_bitrig t05 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig7 : ∀t2.t06 = t2 → eq_bitrig t06 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig8 : ∀t2.t07 = t2 → eq_bitrig t07 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig9 : ∀t2.t08 = t2 → eq_bitrig t08 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig10 : ∀t2.t09 = t2 → eq_bitrig t09 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig11 : ∀t2.t0A = t2 → eq_bitrig t0A t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig12 : ∀t2.t0B = t2 → eq_bitrig t0B t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig13 : ∀t2.t0C = t2 → eq_bitrig t0C t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig14 : ∀t2.t0D = t2 → eq_bitrig t0D t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig15 : ∀t2.t0E = t2 → eq_bitrig t0E t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig16 : ∀t2.t0F = t2 → eq_bitrig t0F t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig17 : ∀t2.t10 = t2 → eq_bitrig t10 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig18 : ∀t2.t11 = t2 → eq_bitrig t11 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig19 : ∀t2.t12 = t2 → eq_bitrig t12 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig20 : ∀t2.t13 = t2 → eq_bitrig t13 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig21 : ∀t2.t14 = t2 → eq_bitrig t14 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+nlemma eq_to_eqbitrig22 : ∀t2.t15 = t2 → eq_bitrig t15 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig23 : ∀t2.t16 = t2 → eq_bitrig t16 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig24 : ∀t2.t17 = t2 → eq_bitrig t17 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig25 : ∀t2.t18 = t2 → eq_bitrig t18 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig26 : ∀t2.t19 = t2 → eq_bitrig t19 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig27 : ∀t2.t1A = t2 → eq_bitrig t1A t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig28 : ∀t2.t1B = t2 → eq_bitrig t1B t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig29 : ∀t2.t1C = t2 → eq_bitrig t1C t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig30 : ∀t2.t1D = t2 → eq_bitrig t1D t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig31 : ∀t2.t1E = t2 → eq_bitrig t1E t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
+nlemma eq_to_eqbitrig32 : ∀t2.t1F = t2 → eq_bitrig t1F t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+nqed.
+
 nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
- #t1; #t2;
+ #t1;
  ncases t1;
- ##[ ##1: ncases t2; nnormalize; #H;
-          ##[ ##1: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##2: ncases t2; nnormalize; #H;
-          ##[ ##2: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]          
- ##| ##3: ncases t2; nnormalize; #H;
-          ##[ ##3: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##4: ncases t2; nnormalize; #H;
-          ##[ ##4: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##5: ncases t2; nnormalize; #H;
-          ##[ ##5: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##6: ncases t2; nnormalize; #H;
-          ##[ ##6: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##7: ncases t2; nnormalize; #H;
-          ##[ ##7: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##8: ncases t2; nnormalize; #H;
-          ##[ ##8: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##9: ncases t2; nnormalize; #H;
-          ##[ ##9: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##10: ncases t2; nnormalize; #H;
-          ##[ ##10: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##11: ncases t2; nnormalize; #H;
-          ##[ ##11: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]            
- ##| ##12: ncases t2; nnormalize; #H;
-          ##[ ##12: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##13: ncases t2; nnormalize; #H;
-          ##[ ##13: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##14: ncases t2; nnormalize; #H;
-          ##[ ##14: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##15: ncases t2; nnormalize; #H;
-          ##[ ##15: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]            
- ##| ##16: ncases t2; nnormalize; #H;
-          ##[ ##16: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##17: ncases t2; nnormalize; #H;
-          ##[ ##17: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##18: ncases t2; nnormalize; #H;
-          ##[ ##18: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##19: ncases t2; nnormalize; #H;
-          ##[ ##19: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]            
- ##| ##20: ncases t2; nnormalize; #H;
-          ##[ ##20: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##21: ncases t2; nnormalize; #H;
-          ##[ ##21: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##22: ncases t2; nnormalize; #H;
-          ##[ ##22: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##23: ncases t2; nnormalize; #H;
-          ##[ ##23: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##24: ncases t2; nnormalize; #H;
-          ##[ ##24: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##25: ncases t2; nnormalize; #H;
-          ##[ ##25: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##26: ncases t2; nnormalize; #H;
-          ##[ ##26: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##27: ncases t2; nnormalize; #H;
-          ##[ ##27: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##28: ncases t2; nnormalize; #H;
-          ##[ ##28: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##29: ncases t2; nnormalize; #H;
-          ##[ ##29: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##30: ncases t2; nnormalize; #H;
-          ##[ ##30: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##31: ncases t2; nnormalize; #H;
-          ##[ ##31: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
- ##| ##32: ncases t2; nnormalize; #H;
-          ##[ ##32: napply (refl_eq ??)
-          ##| ##*: napply (bitrigesim_destruct ??? H)
-          ##]
+ ##[ ##1: napply eq_to_eqbitrig1
+ ##| ##2: napply eq_to_eqbitrig2
+ ##| ##3: napply eq_to_eqbitrig3
+ ##| ##4: napply eq_to_eqbitrig4
+ ##| ##5: napply eq_to_eqbitrig5
+ ##| ##6: napply eq_to_eqbitrig6
+ ##| ##7: napply eq_to_eqbitrig7
+ ##| ##8: napply eq_to_eqbitrig8
+ ##| ##9: napply eq_to_eqbitrig9
+ ##| ##10: napply eq_to_eqbitrig10
+ ##| ##11: napply eq_to_eqbitrig11
+ ##| ##12: napply eq_to_eqbitrig12
+ ##| ##13: napply eq_to_eqbitrig13
+ ##| ##14: napply eq_to_eqbitrig14
+ ##| ##15: napply eq_to_eqbitrig15
+ ##| ##16: napply eq_to_eqbitrig16
+ ##| ##17: napply eq_to_eqbitrig17
+ ##| ##18: napply eq_to_eqbitrig18
+ ##| ##19: napply eq_to_eqbitrig19
+ ##| ##20: napply eq_to_eqbitrig20
+ ##| ##21: napply eq_to_eqbitrig21
+ ##| ##22: napply eq_to_eqbitrig22
+ ##| ##23: napply eq_to_eqbitrig23
+ ##| ##24: napply eq_to_eqbitrig24
+ ##| ##25: napply eq_to_eqbitrig25
+ ##| ##26: napply eq_to_eqbitrig26
+ ##| ##27: napply eq_to_eqbitrig27
+ ##| ##28: napply eq_to_eqbitrig28
+ ##| ##29: napply eq_to_eqbitrig29
+ ##| ##30: napply eq_to_eqbitrig30
+ ##| ##31: napply eq_to_eqbitrig31
+ ##| ##32: napply eq_to_eqbitrig32
  ##]
 nqed.