1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / aux_bases_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
index d94c475e5a747aa09f43656c9f7722f7b2aede51..ce3ea12afdcf743442a5cde350325200825d240a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
@@ -45,49 +45,49 @@ ndefinition oct_destruct : oct_destruct_aux.
  nelim n1;
  ##[ ##1: nelim n2; nnormalize; #H;
           ##[ ##1: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##2: nelim n2; nnormalize; #H;
           ##[ ##2: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##3: nelim n2; nnormalize; #H;
           ##[ ##3: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##4: nelim n2; nnormalize; #H;
           ##[ ##4: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##5: nelim n2; nnormalize; #H;
           ##[ ##5: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##6: nelim n2; nnormalize; #H;
           ##[ ##6: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##7: nelim n2; nnormalize; #H;
           ##[ ##7: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##8: nelim n2; nnormalize; #H;
           ##[ ##8: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply (False_ind …);
                    nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
@@ -99,7 +99,7 @@ nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
  nelim n1;
  nelim n2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
@@ -107,8 +107,8 @@ nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
  ncases n1;
  ncases n2;
  nnormalize;
- ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -117,8 +117,8 @@ nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
  ncases n1;
  ncases n2;
  nnormalize;
- ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (oct_destruct ??? H)
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
+ ##| ##*: #H; napply (oct_destruct … H)
  ##]
 nqed.
 
@@ -132,7 +132,7 @@ ndefinition bitrigesim_destruct1 :
  ncases t2;
  nnormalize; #H;
  ##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -144,7 +144,7 @@ ndefinition bitrigesim_destruct2 :
  ncases t2;
  nnormalize; #H;
  ##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -156,7 +156,7 @@ ndefinition bitrigesim_destruct3 :
  ncases t2;
  nnormalize; #H;
  ##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -168,7 +168,7 @@ ndefinition bitrigesim_destruct4 :
  ncases t2;
  nnormalize; #H;
  ##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -180,7 +180,7 @@ ndefinition bitrigesim_destruct5 :
  ncases t2;
  nnormalize; #H;
  ##[ ##5: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -192,7 +192,7 @@ ndefinition bitrigesim_destruct6 :
  ncases t2;
  nnormalize; #H;
  ##[ ##6: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -204,7 +204,7 @@ ndefinition bitrigesim_destruct7 :
  ncases t2;
  nnormalize; #H;
  ##[ ##7: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -216,7 +216,7 @@ ndefinition bitrigesim_destruct8 :
  ncases t2;
  nnormalize; #H;
  ##[ ##8: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -228,7 +228,7 @@ ndefinition bitrigesim_destruct9 :
  ncases t2;
  nnormalize; #H;
  ##[ ##9: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -240,7 +240,7 @@ ndefinition bitrigesim_destruct10 :
  ncases t2;
  nnormalize; #H;
  ##[ ##10: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -252,7 +252,7 @@ ndefinition bitrigesim_destruct11 :
  ncases t2;
  nnormalize; #H;
  ##[ ##11: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -264,7 +264,7 @@ ndefinition bitrigesim_destruct12 :
  ncases t2;
  nnormalize; #H;
  ##[ ##12: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -276,7 +276,7 @@ ndefinition bitrigesim_destruct13 :
  ncases t2;
  nnormalize; #H;
  ##[ ##13: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -288,7 +288,7 @@ ndefinition bitrigesim_destruct14 :
  ncases t2;
  nnormalize; #H;
  ##[ ##14: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -300,7 +300,7 @@ ndefinition bitrigesim_destruct15 :
  ncases t2;
  nnormalize; #H;
  ##[ ##15: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -312,7 +312,7 @@ ndefinition bitrigesim_destruct16 :
  ncases t2;
  nnormalize; #H;
  ##[ ##16: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -324,7 +324,7 @@ ndefinition bitrigesim_destruct17 :
  ncases t2;
  nnormalize; #H;
  ##[ ##17: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -336,7 +336,7 @@ ndefinition bitrigesim_destruct18 :
  ncases t2;
  nnormalize; #H;
  ##[ ##18: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -348,7 +348,7 @@ ndefinition bitrigesim_destruct19 :
  ncases t2;
  nnormalize; #H;
  ##[ ##19: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -360,7 +360,7 @@ ndefinition bitrigesim_destruct20 :
  ncases t2;
  nnormalize; #H;
  ##[ ##20: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -372,7 +372,7 @@ ndefinition bitrigesim_destruct21 :
  ncases t2;
  nnormalize; #H;
  ##[ ##21: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -384,7 +384,7 @@ ndefinition bitrigesim_destruct22 :
  ncases t2;
  nnormalize; #H;
  ##[ ##22: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -396,7 +396,7 @@ ndefinition bitrigesim_destruct23 :
  ncases t2;
  nnormalize; #H;
  ##[ ##23: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -408,7 +408,7 @@ ndefinition bitrigesim_destruct24 :
  ncases t2;
  nnormalize; #H;
  ##[ ##24: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -420,7 +420,7 @@ ndefinition bitrigesim_destruct25 :
  ncases t2;
  nnormalize; #H;
  ##[ ##25: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -432,7 +432,7 @@ ndefinition bitrigesim_destruct26 :
  ncases t2;
  nnormalize; #H;
  ##[ ##26: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -444,7 +444,7 @@ ndefinition bitrigesim_destruct27 :
  ncases t2;
  nnormalize; #H;
  ##[ ##27: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -456,7 +456,7 @@ ndefinition bitrigesim_destruct28 :
  ncases t2;
  nnormalize; #H;
  ##[ ##28: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -468,7 +468,7 @@ ndefinition bitrigesim_destruct29 :
  ncases t2;
  nnormalize; #H;
  ##[ ##29: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -480,7 +480,7 @@ ndefinition bitrigesim_destruct30 :
  ncases t2;
  nnormalize; #H;
  ##[ ##30: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -492,7 +492,7 @@ ndefinition bitrigesim_destruct31 :
  ncases t2;
  nnormalize; #H;
  ##[ ##31: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -504,7 +504,7 @@ ndefinition bitrigesim_destruct32 :
  ncases t2;
  nnormalize; #H;
  ##[ ##32: napply (λx:P.x)
- ##| ##*: napply (False_ind (λ_.?) ?);
+ ##| ##*: napply (False_ind …);
           nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -588,167 +588,167 @@ nqed.
 nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
  #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 ??)
+ ##[ ##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 eqbitrig_to_eq1 : ∀t2.eq_bitrig t00 t2 = true → t00 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq2 : ∀t2.eq_bitrig t01 t2 = true → t01 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq3 : ∀t2.eq_bitrig t02 t2 = true → t02 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq4 : ∀t2.eq_bitrig t03 t2 = true → t03 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq5 : ∀t2.eq_bitrig t04 t2 = true → t04 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq6 : ∀t2.eq_bitrig t05 t2 = true → t05 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq7 : ∀t2.eq_bitrig t06 t2 = true → t06 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq8 : ∀t2.eq_bitrig t07 t2 = true → t07 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq9 : ∀t2.eq_bitrig t08 t2 = true → t08 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq10 : ∀t2.eq_bitrig t09 t2 = true → t09 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq11 : ∀t2.eq_bitrig t0A t2 = true → t0A = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq12 : ∀t2.eq_bitrig t0B t2 = true → t0B = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq13 : ∀t2.eq_bitrig t0C t2 = true → t0C = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq14 : ∀t2.eq_bitrig t0D t2 = true → t0D = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq15 : ∀t2.eq_bitrig t0E t2 = true → t0E = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq16 : ∀t2.eq_bitrig t0F t2 = true → t0F = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq17 : ∀t2.eq_bitrig t10 t2 = true → t10 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq18 : ∀t2.eq_bitrig t11 t2 = true → t11 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq19 : ∀t2.eq_bitrig t12 t2 = true → t12 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq20 : ∀t2.eq_bitrig t13 t2 = true → t13 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq21 : ∀t2.eq_bitrig t14 t2 = true → t14 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq22 : ∀t2.eq_bitrig t15 t2 = true → t15 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq23 : ∀t2.eq_bitrig t16 t2 = true → t16 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq24 : ∀t2.eq_bitrig t17 t2 = true → t17 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq25 : ∀t2.eq_bitrig t18 t2 = true → t18 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq26 : ∀t2.eq_bitrig t19 t2 = true → t19 = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq27 : ∀t2.eq_bitrig t1A t2 = true → t1A = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq28 : ∀t2.eq_bitrig t1B t2 = true → t1B = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq29 : ∀t2.eq_bitrig t1C t2 = true → t1C = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq30 : ∀t2.eq_bitrig t1D t2 = true → t1D = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq31 : ∀t2.eq_bitrig t1E t2 = true → t1E = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq32 : ∀t2.eq_bitrig t1F t2 = true → t1F = t2.
- #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 nqed.
 
 nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
@@ -790,130 +790,130 @@ nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
 nqed.
 
 nlemma eq_to_eqbitrig1 : ∀t2.t00 = t2 → eq_bitrig t00 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig2 : ∀t2.t01 = t2 → eq_bitrig t01 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig3 : ∀t2.t02 = t2 → eq_bitrig t02 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig4 : ∀t2.t03 = t2 → eq_bitrig t03 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig5 : ∀t2.t04 = t2 → eq_bitrig t04 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig6 : ∀t2.t05 = t2 → eq_bitrig t05 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig7 : ∀t2.t06 = t2 → eq_bitrig t06 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig8 : ∀t2.t07 = t2 → eq_bitrig t07 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig9 : ∀t2.t08 = t2 → eq_bitrig t08 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig10 : ∀t2.t09 = t2 → eq_bitrig t09 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig11 : ∀t2.t0A = t2 → eq_bitrig t0A t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig12 : ∀t2.t0B = t2 → eq_bitrig t0B t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig13 : ∀t2.t0C = t2 → eq_bitrig t0C t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig14 : ∀t2.t0D = t2 → eq_bitrig t0D t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig15 : ∀t2.t0E = t2 → eq_bitrig t0E t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig16 : ∀t2.t0F = t2 → eq_bitrig t0F t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig17 : ∀t2.t10 = t2 → eq_bitrig t10 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig18 : ∀t2.t11 = t2 → eq_bitrig t11 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig19 : ∀t2.t12 = t2 → eq_bitrig t12 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig20 : ∀t2.t13 = t2 → eq_bitrig t13 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig21 : ∀t2.t14 = t2 → eq_bitrig t14 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 nlemma eq_to_eqbitrig22 : ∀t2.t15 = t2 → eq_bitrig t15 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig23 : ∀t2.t16 = t2 → eq_bitrig t16 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig24 : ∀t2.t17 = t2 → eq_bitrig t17 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig25 : ∀t2.t18 = t2 → eq_bitrig t18 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig26 : ∀t2.t19 = t2 → eq_bitrig t19 t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig27 : ∀t2.t1A = t2 → eq_bitrig t1A t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig28 : ∀t2.t1B = t2 → eq_bitrig t1B t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig29 : ∀t2.t1C = t2 → eq_bitrig t1C t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig30 : ∀t2.t1D = t2 → eq_bitrig t1D t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig31 : ∀t2.t1E = t2 → eq_bitrig t1E t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig32 : ∀t2.t1F = t2 → eq_bitrig t1F t2 = true.
- #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 nqed.
 
 nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.