napply (refl_eq ??).
nqed.
-nlemma eqoct_to_eq : ∀o1,o2.eq_oct o1 o2 = true → o1 = o2.
- #n1; #n2; #H;
- nletin K ≝ (bool_destruct ?? (n1 = n2) H);
- nelim n1 in K:(%) ⊢ %;
- nelim n2;
+nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
- #n1; #n2; #H;
- nletin K ≝ (oct_destruct ?? (eq_oct n1 n2 = true) H);
- nelim n1 in K:(%) ⊢ %;
- nelim n2;
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (oct_destruct ??? H)
##]
nqed.
nqed.
nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
- #t1; #t2; #H;
- nletin K ≝ (bool_destruct ?? (t1 = t2) H);
- nelim t1 in K:(%) ⊢ %;
- ##[ ##1: nelim t2; nnormalize; #H;
+ #t1; #t2;
+ ncases t1;
+ ##[ ##1: ncases t2; nnormalize; #H;
##[ ##1: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##2: nelim t2; nnormalize; #H;
+ ##| ##2: ncases t2; nnormalize; #H;
##[ ##2: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##3: nelim t2; nnormalize; #H;
+ ##| ##3: ncases t2; nnormalize; #H;
##[ ##3: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##4: nelim t2; nnormalize; #H;
+ ##| ##4: ncases t2; nnormalize; #H;
##[ ##4: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##5: nelim t2; nnormalize; #H;
+ ##| ##5: ncases t2; nnormalize; #H;
##[ ##5: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##6: nelim t2; nnormalize; #H;
+ ##| ##6: ncases t2; nnormalize; #H;
##[ ##6: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*:napply (bool_destruct ??? H)
##]
- ##| ##7: nelim t2; nnormalize; #H;
+ ##| ##7: ncases t2; nnormalize; #H;
##[ ##7: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##8: nelim t2; nnormalize; #H;
+ ##| ##8: ncases t2; nnormalize; #H;
##[ ##8: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##9: nelim t2; nnormalize; #H;
+ ##| ##9: ncases t2; nnormalize; #H;
##[ ##9: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##10: nelim t2; nnormalize; #H;
+ ##| ##10: ncases t2; nnormalize; #H;
##[ ##10: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##11: nelim t2; nnormalize; #H;
+ ##| ##11: ncases t2; nnormalize; #H;
##[ ##11: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##12: nelim t2; nnormalize; #H;
+ ##| ##12: ncases t2; nnormalize; #H;
##[ ##12: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##13: nelim t2; nnormalize; #H;
+ ##| ##13: ncases t2; nnormalize; #H;
##[ ##13: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##14: nelim t2; nnormalize; #H;
+ ##| ##14: ncases t2; nnormalize; #H;
##[ ##14: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##15: nelim t2; nnormalize; #H;
+ ##| ##15: ncases t2; nnormalize; #H;
##[ ##15: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##16: nelim t2; nnormalize; #H;
+ ##| ##16: ncases t2; nnormalize; #H;
##[ ##16: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##17: nelim t2; nnormalize; #H;
+ ##| ##17: ncases t2; nnormalize; #H;
##[ ##17: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##18: nelim t2; nnormalize; #H;
+ ##| ##18: ncases t2; nnormalize; #H;
##[ ##18: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##19: nelim t2; nnormalize; #H;
+ ##| ##19: ncases t2; nnormalize; #H;
##[ ##19: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##20: nelim t2; nnormalize; #H;
+ ##| ##20: ncases t2; nnormalize; #H;
##[ ##20: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##21: nelim t2; nnormalize; #H;
+ ##| ##21: ncases t2; nnormalize; #H;
##[ ##21: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##22: nelim t2; nnormalize; #H;
+ ##| ##22: ncases t2; nnormalize; #H;
##[ ##22: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##23: nelim t2; nnormalize; #H;
+ ##| ##23: ncases t2; nnormalize; #H;
##[ ##23: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##24: nelim t2; nnormalize; #H;
+ ##| ##24: ncases t2; nnormalize; #H;
##[ ##24: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##25: nelim t2; nnormalize; #H;
+ ##| ##25: ncases t2; nnormalize; #H;
##[ ##25: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##26: nelim t2; nnormalize; #H;
+ ##| ##26: ncases t2; nnormalize; #H;
##[ ##26: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##27: nelim t2; nnormalize; #H;
+ ##| ##27: ncases t2; nnormalize; #H;
##[ ##27: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##28: nelim t2; nnormalize; #H;
+ ##| ##28: ncases t2; nnormalize; #H;
##[ ##28: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##29: nelim t2; nnormalize; #H;
+ ##| ##29: ncases t2; nnormalize; #H;
##[ ##29: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##30: nelim t2; nnormalize; #H;
+ ##| ##30: ncases t2; nnormalize; #H;
##[ ##30: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##31: nelim t2; nnormalize; #H;
+ ##| ##31: ncases t2; nnormalize; #H;
##[ ##31: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##32: nelim t2; nnormalize; #H;
+ ##| ##32: ncases t2; nnormalize; #H;
##[ ##32: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
##]
nqed.
nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
- #t1; #t2; #H;
- nletin K ≝ (bitrigesim_destruct ?? (eq_bitrig t1 t2 = true) H);
- nelim t1 in K:(%) ⊢ %;
- ##[ ##1: nelim t2; nnormalize; #H;
+ #t1; #t2;
+ ncases t1;
+ ##[ ##1: ncases t2; nnormalize; #H;
##[ ##1: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##2: nelim t2; nnormalize; #H;
+ ##| ##2: ncases t2; nnormalize; #H;
##[ ##2: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##3: nelim t2; nnormalize; #H;
+ ##| ##3: ncases t2; nnormalize; #H;
##[ ##3: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##4: nelim t2; nnormalize; #H;
+ ##| ##4: ncases t2; nnormalize; #H;
##[ ##4: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##5: nelim t2; nnormalize; #H;
+ ##| ##5: ncases t2; nnormalize; #H;
##[ ##5: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##6: nelim t2; nnormalize; #H;
+ ##| ##6: ncases t2; nnormalize; #H;
##[ ##6: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##7: nelim t2; nnormalize; #H;
+ ##| ##7: ncases t2; nnormalize; #H;
##[ ##7: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##8: nelim t2; nnormalize; #H;
+ ##| ##8: ncases t2; nnormalize; #H;
##[ ##8: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##9: nelim t2; nnormalize; #H;
+ ##| ##9: ncases t2; nnormalize; #H;
##[ ##9: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##10: nelim t2; nnormalize; #H;
+ ##| ##10: ncases t2; nnormalize; #H;
##[ ##10: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##11: nelim t2; nnormalize; #H;
+ ##| ##11: ncases t2; nnormalize; #H;
##[ ##11: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##12: nelim t2; nnormalize; #H;
+ ##| ##12: ncases t2; nnormalize; #H;
##[ ##12: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##13: nelim t2; nnormalize; #H;
+ ##| ##13: ncases t2; nnormalize; #H;
##[ ##13: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##14: nelim t2; nnormalize; #H;
+ ##| ##14: ncases t2; nnormalize; #H;
##[ ##14: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##15: nelim t2; nnormalize; #H;
+ ##| ##15: ncases t2; nnormalize; #H;
##[ ##15: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##16: nelim t2; nnormalize; #H;
+ ##| ##16: ncases t2; nnormalize; #H;
##[ ##16: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##17: nelim t2; nnormalize; #H;
+ ##| ##17: ncases t2; nnormalize; #H;
##[ ##17: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##18: nelim t2; nnormalize; #H;
+ ##| ##18: ncases t2; nnormalize; #H;
##[ ##18: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##19: nelim t2; nnormalize; #H;
+ ##| ##19: ncases t2; nnormalize; #H;
##[ ##19: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##20: nelim t2; nnormalize; #H;
+ ##| ##20: ncases t2; nnormalize; #H;
##[ ##20: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##21: nelim t2; nnormalize; #H;
+ ##| ##21: ncases t2; nnormalize; #H;
##[ ##21: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##22: nelim t2; nnormalize; #H;
+ ##| ##22: ncases t2; nnormalize; #H;
##[ ##22: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##23: nelim t2; nnormalize; #H;
+ ##| ##23: ncases t2; nnormalize; #H;
##[ ##23: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##24: nelim t2; nnormalize; #H;
+ ##| ##24: ncases t2; nnormalize; #H;
##[ ##24: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##25: nelim t2; nnormalize; #H;
+ ##| ##25: ncases t2; nnormalize; #H;
##[ ##25: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##26: nelim t2; nnormalize; #H;
+ ##| ##26: ncases t2; nnormalize; #H;
##[ ##26: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##27: nelim t2; nnormalize; #H;
+ ##| ##27: ncases t2; nnormalize; #H;
##[ ##27: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##28: nelim t2; nnormalize; #H;
+ ##| ##28: ncases t2; nnormalize; #H;
##[ ##28: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##29: nelim t2; nnormalize; #H;
+ ##| ##29: ncases t2; nnormalize; #H;
##[ ##29: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##30: nelim t2; nnormalize; #H;
+ ##| ##30: ncases t2; nnormalize; #H;
##[ ##30: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##31: nelim t2; nnormalize; #H;
+ ##| ##31: ncases t2; nnormalize; #H;
##[ ##31: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##32: nelim t2; nnormalize; #H;
+ ##| ##32: ncases t2; nnormalize; #H;
##[ ##32: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
##]
nqed.