-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