1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma
index d00d67bb9882197ac8645a679e7f4e50786f54b7..289cfaf6579def97e6549eee454ac2a0695b6cbf 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma
@@ -53,7 +53,7 @@ nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1
  nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2.
@@ -61,7 +61,7 @@ nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1
  nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
@@ -71,7 +71,7 @@ nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
   ((eq_str (str_elem si2) (str_elem si1))⊗(eq_nat (id_elem si2) (id_elem si1))));
  nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
  nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed. 
 
 nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
@@ -81,9 +81,9 @@ nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
  nelim si2;
  #l2; #n2; #H;
  nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
- nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l ?? H));
- nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r ?? H));
- napply (refl_eq ??).
+ nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l … H));
+ nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H));
+ napply refl_eq.
 nqed.
 
 nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
@@ -93,10 +93,10 @@ nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
  nelim si2;
  #l2; #n2; #H;
  nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
- nrewrite > (strid_destruct_1 ???? H);
- nrewrite > (strid_destruct_2 ???? H);
- nrewrite > (eq_to_eqstr l2 l2 (refl_eq ??));
- nrewrite > (eq_to_eqnat n2 n2 (refl_eq ??));
+ nrewrite > (strid_destruct_1 … H);
+ nrewrite > (strid_destruct_2 … H);
+ nrewrite > (eq_to_eqstr l2 l2 (refl_eq …));
+ nrewrite > (eq_to_eqnat n2 n2 (refl_eq …));
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.