(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / common / prod_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
index b73d1347f58269eee3f933bbf74bad840709f49f..29998a836f9cc4f9b3f54e7cc9880aa9680a4f28 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -101,7 +101,7 @@ nlemma eqpair_to_eq :
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
  #H3;
- ##[ ##2: napply (bool_destruct … H3) ##]
+ ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
  #H4;
  nrewrite > (H4 (refl_eq …));
  nrewrite > (H2 y1 y2 H3);
@@ -282,11 +282,11 @@ nlemma eqtriple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H4; napply (bool_destruct … H4) ##]
+ ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
+ ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
  #H4; #H5; #H6;
  nrewrite > (H4 (refl_eq …));
  nrewrite > (H6 (refl_eq …));
@@ -507,15 +507,15 @@ nlemma eqquadruple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H5; napply (bool_destruct … H5) ##]
+ ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
+ ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
+ ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
  #H5; #H6; #H7; #H8;
  nrewrite > (H5 (refl_eq …));
  nrewrite > (H6 (refl_eq …));
@@ -775,19 +775,19 @@ nlemma eqquintuple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H6; napply (bool_destruct … H6) ##]
+ ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
+ ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
+ ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
  nletin K3 ≝ (H4 v1 v2);
  ncases (f4 v1 v2) in K3:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
+ ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
  #H6; #H7; #H8; #H9; #H10;
  nrewrite > (H6 (refl_eq …));
  nrewrite > (H7 (refl_eq …));