-nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
- #t1;
- nelim t1;
- ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
- ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
- ##]
-nqed.
-
-nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-nqed.
-
-nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
-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
- ##]
-nqed.
-
-nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-nqed.
-
-nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
-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
- ##]
-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)
- ##]