X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbitrigesim_lemmas.ma;h=5eecaff9160d2ec82a5eb69b683aa96bb77987ce;hb=417792b30223b5edd4a9194193c7f34514bd0fa3;hp=675f14fb37049f638d4c10c81f29a32bb49e7b95;hpb=b1c174cffd3c1d10383a52d63a6e662156fb0bb7;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 675f14fb3..5eecaff91 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,831 +27,109 @@ include "num/bool_lemmas.ma".
 (* BITRIGESIMALI *)
 (* ************* *)
 
-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 ]
-  | 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 ]
-  ].
+ match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ 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
- ##]
-nqed.
-
-nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
- #t1;
+ #t1; #t2; #P; #H;
+ nrewrite < H;
  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.
+ nnormalize;
+ napply (λx.x).
+nqed.
+
+nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_bit n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqbit n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+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
+ #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) ##]
+nlemma neq_to_neqbit : ∀n1,n2.n1 ≠ n2 → eq_bit n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_bit n1 n2));
+ napply (not_to_not (eq_bit n1 n2 = true) (n1 = n2) ? H);
+ napply (eqbit_to_eq n1 n2).
 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) ##]
+nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_bit x y = true) (eq_bit x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqbit_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqbit_to_neq … 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
+nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_bit n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqbit n1 n2 H);
+          napply (symmetric_eq ? (eq_bit n2 n1) false);
+          napply (neq_to_neqbit n2 n1 (symmetric_neq ? n1 n2 H))
  ##]
 nqed.