X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbitrigesim_lemmas.ma;h=812f31a9d7e83ac2d63ba7d01d79e96274444974;hb=29cfb9e2961e62c836cb50217905c0594a074e81;hp=08f88acfd62088f3b3bdd991b66eb03b872a510a;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
index 08f88acfd..812f31a9d 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
@@ -414,75 +414,43 @@ 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 ]
-  | 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 ]
+  [ 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 ]
   ].
 
 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
+ ##[ ##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.
 
@@ -653,40 +621,23 @@ nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
 nqed.
 
 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
- #t1;
- ncases t1;
- ##[ ##1: napply eqbit_to_eq1
- ##| ##2: napply eqbit_to_eq2
- ##| ##3: napply eqbit_to_eq3
- ##| ##4: napply eqbit_to_eq4
- ##| ##5: napply eqbit_to_eq5
- ##| ##6: napply eqbit_to_eq6
- ##| ##7: napply eqbit_to_eq7
- ##| ##8: napply eqbit_to_eq8
- ##| ##9: napply eqbit_to_eq9
- ##| ##10: napply eqbit_to_eq10
- ##| ##11: napply eqbit_to_eq11
- ##| ##12: napply eqbit_to_eq12
- ##| ##13: napply eqbit_to_eq13
- ##| ##14: napply eqbit_to_eq14
- ##| ##15: napply eqbit_to_eq15
- ##| ##16: napply eqbit_to_eq16
- ##| ##17: napply eqbit_to_eq17
- ##| ##18: napply eqbit_to_eq18
- ##| ##19: napply eqbit_to_eq19
- ##| ##20: napply eqbit_to_eq20
- ##| ##21: napply eqbit_to_eq21
- ##| ##22: napply eqbit_to_eq22
- ##| ##23: napply eqbit_to_eq23
- ##| ##24: napply eqbit_to_eq24
- ##| ##25: napply eqbit_to_eq25
- ##| ##26: napply eqbit_to_eq26
- ##| ##27: napply eqbit_to_eq27
- ##| ##28: napply eqbit_to_eq28
- ##| ##29: napply eqbit_to_eq29
- ##| ##30: napply eqbit_to_eq30
- ##| ##31: napply eqbit_to_eq31
- ##| ##32: napply eqbit_to_eq32
+ #t1; ncases t1;
+ ##[ ##1: napply eqbit_to_eq1 ##| ##2: napply eqbit_to_eq2
+ ##| ##3: napply eqbit_to_eq3 ##| ##4: napply eqbit_to_eq4
+ ##| ##5: napply eqbit_to_eq5 ##| ##6: napply eqbit_to_eq6
+ ##| ##7: napply eqbit_to_eq7 ##| ##8: napply eqbit_to_eq8
+ ##| ##9: napply eqbit_to_eq9 ##| ##10: napply eqbit_to_eq10
+ ##| ##11: napply eqbit_to_eq11 ##| ##12: napply eqbit_to_eq12
+ ##| ##13: napply eqbit_to_eq13 ##| ##14: napply eqbit_to_eq14
+ ##| ##15: napply eqbit_to_eq15 ##| ##16: napply eqbit_to_eq16
+ ##| ##17: napply eqbit_to_eq17 ##| ##18: napply eqbit_to_eq18
+ ##| ##19: napply eqbit_to_eq19 ##| ##20: napply eqbit_to_eq20
+ ##| ##21: napply eqbit_to_eq21 ##| ##22: napply eqbit_to_eq22
+ ##| ##23: napply eqbit_to_eq23 ##| ##24: napply eqbit_to_eq24
+ ##| ##25: napply eqbit_to_eq25 ##| ##26: napply eqbit_to_eq26
+ ##| ##27: napply eqbit_to_eq27 ##| ##28: napply eqbit_to_eq28
+ ##| ##29: napply eqbit_to_eq29 ##| ##30: napply eqbit_to_eq30
+ ##| ##31: napply eqbit_to_eq31 ##| ##32: napply eqbit_to_eq32
  ##]
 nqed.
 
@@ -819,39 +770,661 @@ nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
 nqed.
 
 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
- #t1;
- ncases t1;
- ##[ ##1: napply eq_to_eqbit1
- ##| ##2: napply eq_to_eqbit2
- ##| ##3: napply eq_to_eqbit3
- ##| ##4: napply eq_to_eqbit4
- ##| ##5: napply eq_to_eqbit5
- ##| ##6: napply eq_to_eqbit6
- ##| ##7: napply eq_to_eqbit7
- ##| ##8: napply eq_to_eqbit8
- ##| ##9: napply eq_to_eqbit9
- ##| ##10: napply eq_to_eqbit10
- ##| ##11: napply eq_to_eqbit11
- ##| ##12: napply eq_to_eqbit12
- ##| ##13: napply eq_to_eqbit13
- ##| ##14: napply eq_to_eqbit14
- ##| ##15: napply eq_to_eqbit15
- ##| ##16: napply eq_to_eqbit16
- ##| ##17: napply eq_to_eqbit17
- ##| ##18: napply eq_to_eqbit18
- ##| ##19: napply eq_to_eqbit19
- ##| ##20: napply eq_to_eqbit20
- ##| ##21: napply eq_to_eqbit21
- ##| ##22: napply eq_to_eqbit22
- ##| ##23: napply eq_to_eqbit23
- ##| ##24: napply eq_to_eqbit24
- ##| ##25: napply eq_to_eqbit25
- ##| ##26: napply eq_to_eqbit26
- ##| ##27: napply eq_to_eqbit27
- ##| ##28: napply eq_to_eqbit28
- ##| ##29: napply eq_to_eqbit29
- ##| ##30: napply eq_to_eqbit30
- ##| ##31: napply eq_to_eqbit31
- ##| ##32: napply eq_to_eqbit32
+ #t1; ncases t1;
+ ##[ ##1: napply eq_to_eqbit1 ##| ##2: napply eq_to_eqbit2
+ ##| ##3: napply eq_to_eqbit3 ##| ##4: napply eq_to_eqbit4
+ ##| ##5: napply eq_to_eqbit5 ##| ##6: napply eq_to_eqbit6
+ ##| ##7: napply eq_to_eqbit7 ##| ##8: napply eq_to_eqbit8
+ ##| ##9: napply eq_to_eqbit9 ##| ##10: napply eq_to_eqbit10
+ ##| ##11: napply eq_to_eqbit11 ##| ##12: napply eq_to_eqbit12
+ ##| ##13: napply eq_to_eqbit13 ##| ##14: napply eq_to_eqbit14
+ ##| ##15: napply eq_to_eqbit15 ##| ##16: napply eq_to_eqbit16
+ ##| ##17: napply eq_to_eqbit17 ##| ##18: napply eq_to_eqbit18
+ ##| ##19: napply eq_to_eqbit19 ##| ##20: napply eq_to_eqbit20
+ ##| ##21: napply eq_to_eqbit21 ##| ##22: napply eq_to_eqbit22
+ ##| ##23: napply eq_to_eqbit23 ##| ##24: napply eq_to_eqbit24
+ ##| ##25: napply eq_to_eqbit25 ##| ##26: napply eq_to_eqbit26
+ ##| ##27: napply eq_to_eqbit27 ##| ##28: napply eq_to_eqbit28
+ ##| ##29: napply eq_to_eqbit29 ##| ##30: napply eq_to_eqbit30
+ ##| ##31: napply eq_to_eqbit31 ##| ##32: napply eq_to_eqbit32
+ ##]
+nqed.
+
+nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
+ #x; nnormalize; nelim x;
+ ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
+ #x; nnormalize; nelim x;
+ ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
+ #x; nnormalize; nelim x;
+ ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
+ #x; nnormalize; nelim x;
+ ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
+ #x; nnormalize; nelim x;
+ ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
+ #x; nnormalize; nelim x;
+ ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
+ #x; nnormalize; nelim x;
+ ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
+ #x; nnormalize; nelim x;
+ ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
+ #x; nnormalize; nelim x;
+ ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
+ #x; nnormalize; nelim x;
+ ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
+ #x; nnormalize; nelim x;
+ ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
+ #x; nnormalize; nelim x;
+ ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
+ #x; nnormalize; nelim x;
+ ##[ ##1: napply decidable_bit1 ##| ##2: napply decidable_bit2
+ ##| ##3: napply decidable_bit3 ##| ##4: napply decidable_bit4
+ ##| ##5: napply decidable_bit5 ##| ##6: napply decidable_bit6
+ ##| ##7: napply decidable_bit7 ##| ##8: napply decidable_bit8
+ ##| ##9: napply decidable_bit9 ##| ##10: napply decidable_bit10
+ ##| ##11: napply decidable_bit11 ##| ##12: napply decidable_bit12
+ ##| ##13: napply decidable_bit13 ##| ##14: napply decidable_bit14
+ ##| ##15: napply decidable_bit15 ##| ##16: napply decidable_bit16
+ ##| ##17: napply decidable_bit17 ##| ##18: napply decidable_bit18
+ ##| ##19: napply decidable_bit19 ##| ##20: napply decidable_bit20
+ ##| ##21: napply decidable_bit21 ##| ##22: napply decidable_bit22
+ ##| ##23: napply decidable_bit23 ##| ##24: napply decidable_bit24
+ ##| ##25: napply decidable_bit25 ##| ##26: napply decidable_bit26
+ ##| ##27: napply decidable_bit27 ##| ##28: napply decidable_bit28
+ ##| ##29: napply decidable_bit29 ##| ##30: napply decidable_bit30
+ ##| ##31: napply decidable_bit31 ##| ##32: napply decidable_bit32
+ ##]
+nqed.
+
+nlemma neqbit_to_neq1 : ∀t2.eq_bit t00 t2 = false → t00 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##1: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq2 : ∀t2.eq_bit t01 t2 = false → t01 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##2: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq3 : ∀t2.eq_bit t02 t2 = false → t02 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##3: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq4 : ∀t2.eq_bit t03 t2 = false → t03 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##4: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq5 : ∀t2.eq_bit t04 t2 = false → t04 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##5: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq6 : ∀t2.eq_bit t05 t2 = false → t05 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##6: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq7 : ∀t2.eq_bit t06 t2 = false → t06 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##7: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq8 : ∀t2.eq_bit t07 t2 = false → t07 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##8: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq9 : ∀t2.eq_bit t08 t2 = false → t08 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##9: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq10 : ∀t2.eq_bit t09 t2 = false → t09 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##10: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq11 : ∀t2.eq_bit t0A t2 = false → t0A ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##11: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq12 : ∀t2.eq_bit t0B t2 = false → t0B ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##12: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq13 : ∀t2.eq_bit t0C t2 = false → t0C ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##13: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq14 : ∀t2.eq_bit t0D t2 = false → t0D ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##14: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq15 : ∀t2.eq_bit t0E t2 = false → t0E ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##15: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq16 : ∀t2.eq_bit t0F t2 = false → t0F ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##16: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq17 : ∀t2.eq_bit t10 t2 = false → t10 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##17: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq18 : ∀t2.eq_bit t11 t2 = false → t11 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##18: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq19 : ∀t2.eq_bit t12 t2 = false → t12 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##19: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq20 : ∀t2.eq_bit t13 t2 = false → t13 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##20: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq21 : ∀t2.eq_bit t14 t2 = false → t14 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##21: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq22 : ∀t2.eq_bit t15 t2 = false → t15 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##22: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq23 : ∀t2.eq_bit t16 t2 = false → t16 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##23: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq24 : ∀t2.eq_bit t17 t2 = false → t17 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##24: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq25 : ∀t2.eq_bit t18 t2 = false → t18 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##25: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq26 : ∀t2.eq_bit t19 t2 = false → t19 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##26: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq27 : ∀t2.eq_bit t1A t2 = false → t1A ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##27: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq28 : ∀t2.eq_bit t1B t2 = false → t1B ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##28: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq29 : ∀t2.eq_bit t1C t2 = false → t1C ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##29: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq30 : ∀t2.eq_bit t1D t2 = false → t1D ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##30: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq31 : ∀t2.eq_bit t1E t2 = false → t1E ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##31: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq32 : ∀t2.eq_bit t1F t2 = false → t1F ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##32: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
+ #t1; nelim t1;
+ ##[ ##1: napply neqbit_to_neq1 ##| ##2: napply neqbit_to_neq2
+ ##| ##3: napply neqbit_to_neq3 ##| ##4: napply neqbit_to_neq4
+ ##| ##5: napply neqbit_to_neq5 ##| ##6: napply neqbit_to_neq6
+ ##| ##7: napply neqbit_to_neq7 ##| ##8: napply neqbit_to_neq8
+ ##| ##9: napply neqbit_to_neq9 ##| ##10: napply neqbit_to_neq10
+ ##| ##11: napply neqbit_to_neq11 ##| ##12: napply neqbit_to_neq12
+ ##| ##13: napply neqbit_to_neq13 ##| ##14: napply neqbit_to_neq14
+ ##| ##15: napply neqbit_to_neq15 ##| ##16: napply neqbit_to_neq16
+ ##| ##17: napply neqbit_to_neq17 ##| ##18: napply neqbit_to_neq18
+ ##| ##19: napply neqbit_to_neq19 ##| ##20: napply neqbit_to_neq20
+ ##| ##21: napply neqbit_to_neq21 ##| ##22: napply neqbit_to_neq22
+ ##| ##23: napply neqbit_to_neq23 ##| ##24: napply neqbit_to_neq24
+ ##| ##25: napply neqbit_to_neq25 ##| ##26: napply neqbit_to_neq26
+ ##| ##27: napply neqbit_to_neq27 ##| ##28: napply neqbit_to_neq28
+ ##| ##29: napply neqbit_to_neq29 ##| ##30: napply neqbit_to_neq30
+ ##| ##31: napply neqbit_to_neq31 ##| ##32: napply neqbit_to_neq32
+ ##]
+nqed.
+
+nlemma neq_to_neqbit1 : ∀t2.t00 ≠ t2 → eq_bit t00 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit2 : ∀t2.t01 ≠ t2 → eq_bit t01 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit3 : ∀t2.t02 ≠ t2 → eq_bit t02 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit4 : ∀t2.t03 ≠ t2 → eq_bit t03 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit5 : ∀t2.t04 ≠ t2 → eq_bit t04 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit6 : ∀t2.t05 ≠ t2 → eq_bit t05 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit7 : ∀t2.t06 ≠ t2 → eq_bit t06 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit8 : ∀t2.t07 ≠ t2 → eq_bit t07 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit9 : ∀t2.t08 ≠ t2 → eq_bit t08 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit10 : ∀t2.t09 ≠ t2 → eq_bit t09 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit11 : ∀t2.t0A ≠ t2 → eq_bit t0A t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit12 : ∀t2.t0B ≠ t2 → eq_bit t0B t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit13 : ∀t2.t0C ≠ t2 → eq_bit t0C t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit14 : ∀t2.t0D ≠ t2 → eq_bit t0D t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit15 : ∀t2.t0E ≠ t2 → eq_bit t0E t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit16 : ∀t2.t0F ≠ t2 → eq_bit t0F t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit17 : ∀t2.t10 ≠ t2 → eq_bit t10 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit18 : ∀t2.t11 ≠ t2 → eq_bit t11 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit19 : ∀t2.t12 ≠ t2 → eq_bit t12 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit20 : ∀t2.t13 ≠ t2 → eq_bit t13 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit21 : ∀t2.t14 ≠ t2 → eq_bit t14 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit22 : ∀t2.t15 ≠ t2 → eq_bit t15 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit23 : ∀t2.t16 ≠ t2 → eq_bit t16 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit24 : ∀t2.t17 ≠ t2 → eq_bit t17 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit25 : ∀t2.t18 ≠ t2 → eq_bit t18 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit26 : ∀t2.t19 ≠ t2 → eq_bit t19 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit27 : ∀t2.t1A ≠ t2 → eq_bit t1A t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit28 : ∀t2.t1B ≠ t2 → eq_bit t1B t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit29 : ∀t2.t1C ≠ t2 → eq_bit t1C t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit30 : ∀t2.t1D ≠ t2 → eq_bit t1D t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit31 : ∀t2.t1E ≠ t2 → eq_bit t1E t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit32 : ∀t2.t1F ≠ t2 → eq_bit t1F t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
+ #t1; nelim t1;
+ ##[ ##1: napply neq_to_neqbit1 ##| ##2: napply neq_to_neqbit2
+ ##| ##3: napply neq_to_neqbit3 ##| ##4: napply neq_to_neqbit4
+ ##| ##5: napply neq_to_neqbit5 ##| ##6: napply neq_to_neqbit6
+ ##| ##7: napply neq_to_neqbit7 ##| ##8: napply neq_to_neqbit8
+ ##| ##9: napply neq_to_neqbit9 ##| ##10: napply neq_to_neqbit10
+ ##| ##11: napply neq_to_neqbit11 ##| ##12: napply neq_to_neqbit12
+ ##| ##13: napply neq_to_neqbit13 ##| ##14: napply neq_to_neqbit14
+ ##| ##15: napply neq_to_neqbit15 ##| ##16: napply neq_to_neqbit16
+ ##| ##17: napply neq_to_neqbit17 ##| ##18: napply neq_to_neqbit18
+ ##| ##19: napply neq_to_neqbit19 ##| ##20: napply neq_to_neqbit20
+ ##| ##21: napply neq_to_neqbit21 ##| ##22: napply neq_to_neqbit22
+ ##| ##23: napply neq_to_neqbit23 ##| ##24: napply neq_to_neqbit24
+ ##| ##25: napply neq_to_neqbit25 ##| ##26: napply neq_to_neqbit26
+ ##| ##27: napply neq_to_neqbit27 ##| ##28: napply neq_to_neqbit28
+ ##| ##29: napply neq_to_neqbit29 ##| ##30: napply neq_to_neqbit30
+ ##| ##31: napply neq_to_neqbit31 ##| ##32: napply neq_to_neqbit32
  ##]
 nqed.