1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / utility.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility.ma b/helm/software/matita/contribs/ng_assembly/utility/utility.ma
index 17b96650395d92f9579e90531f50b23c1219048e..35cb725a0f69d9bd996763d07c7f6215934f4858 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/utility.ma
@@ -229,18 +229,18 @@ nlemma fold_right_list2_aux3 :
  #T; #h; #h'; #t; #t';
  nelim t;
  nelim t';
- ##[ ##1: nnormalize; #H; napply (refl_eq ??)
+ ##[ ##1: nnormalize; #H; napply refl_eq
  ##| ##2: #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
-          nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
+          nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
  ##| ##3: #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
-          nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
+          nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
           nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
           nchange with ((S (len_list T l1)) = (S (len_list T l)));
-          nrewrite > (nat_destruct_S_S ?? H2);
-          napply (refl_eq ??)
+          nrewrite > (nat_destruct_S_S … H2);
+          napply refl_eq
  ##]
 nqed.
 
@@ -276,8 +276,8 @@ nlemma fold_right_neList2_aux1 :
  nnormalize;
  ncases t';
  nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H))
+ ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
+ ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
  ##]
 nqed.
 
@@ -287,8 +287,8 @@ nlemma fold_right_neList2_aux2 :
  nnormalize;
  ncases t;
  nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H))
+ ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
+ ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
  ##]
 nqed.
 
@@ -297,19 +297,19 @@ nlemma fold_right_neList2_aux3 :
  #T; #h; #h'; #t; #t';
  nelim t;
  nelim t';
- ##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??)
+ ##[ ##1: nnormalize; #x; #y; #H; napply refl_eq
  ##| ##2: #a; #l'; #H; #x; #H1;
           nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
-          nrewrite > (nat_destruct_S_S ?? H1);
-          napply (refl_eq ??)
+          nrewrite > (nat_destruct_S_S … H1);
+          napply refl_eq
  ##| ##3: #x; #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
-          nrewrite > (nat_destruct_S_S ?? H1);
-          napply (refl_eq ??)
+          nrewrite > (nat_destruct_S_S … H1);
+          napply refl_eq
  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
           nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l))));
-          nrewrite > (nat_destruct_S_S ?? H2);
-          napply (refl_eq ??)
+          nrewrite > (nat_destruct_S_S … H2);
+          napply refl_eq
  ##]
 nqed.