(no commit message)

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
index d95af89a67a15d3e9938caed9c242d8f0e3d0f79..96bc15172b9f334b0f56c3c69b664c4e080bbce0 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
@@ -54,8 +54,8 @@ nqed.
 nlemma bsymmetric_eqpair :
 ∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
- (boolSymmetric T1 f1) →
- (boolSymmetric T2 f2) →
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
  (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
  #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
  ncases p1;
@@ -102,7 +102,7 @@ nlemma eqpair_to_eq :
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
  #H3;
- ##[ ##2: nelim (bool_destruct_false_true H3) ##]
+ ##[ ##2: napply (bool_destruct ??? H3) ##]
  #H4;
  nrewrite > (H4 (refl_eq ??));
  nrewrite > (H2 y1 y2 H3);
@@ -142,9 +142,9 @@ nqed.
 nlemma bsymmetric_eqtriple :
 ∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
- (boolSymmetric T1 f1) →
- (boolSymmetric T2 f2) →
- (boolSymmetric T3 f3) →
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (symmetricT T3 bool f3) →
  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
  ncases p1;
@@ -199,11 +199,11 @@ nlemma eqtriple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H4; nelim (bool_destruct_false_true H4) ##]
+ ##[ ##2: #H4; napply (bool_destruct ??? H4) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H4; #H5; nelim (bool_destruct_false_true H5) ##]
+ ##[ ##2: #H4; #H5; napply (bool_destruct ??? H5) ##]
  #H4; #H5; #H6;
  nrewrite > (H4 (refl_eq ??));
  nrewrite > (H6 (refl_eq ??));
@@ -254,10 +254,10 @@ nqed.
 nlemma bsymmetric_eqquadruple :
 ∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
- (boolSymmetric T1 f1) →
- (boolSymmetric T2 f2) →
- (boolSymmetric T3 f3) →
- (boolSymmetric T4 f4) →
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (symmetricT T3 bool f3) →
+ (symmetricT T4 bool f4) →
  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
  ncases p1;
@@ -321,15 +321,15 @@ nlemma eqquadruple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H5; nelim (bool_destruct_false_true H5) ##]
+ ##[ ##2: #H5; napply (bool_destruct ??? H5) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; nelim (bool_destruct_false_true H6) ##]
+ ##[ ##2: #H5; #H6; napply (bool_destruct ??? H6) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; #H7; nelim (bool_destruct_false_true H7) ##]
+ ##[ ##2: #H5; #H6; #H7; napply (bool_destruct ??? H7) ##]
  #H5; #H6; #H7; #H8;
  nrewrite > (H5 (refl_eq ??));
  nrewrite > (H6 (refl_eq ??));
@@ -391,11 +391,11 @@ nqed.
 nlemma bsymmetric_eqquintuple :
 ∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
- (boolSymmetric T1 f1) →
- (boolSymmetric T2 f2) →
- (boolSymmetric T3 f3) →
- (boolSymmetric T4 f4) →
- (boolSymmetric T5 f5) →
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (symmetricT T3 bool f3) →
+ (symmetricT T4 bool f4) →
+ (symmetricT T5 bool f5) →
  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
  ncases p1;
@@ -468,19 +468,19 @@ nlemma eqquintuple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H6; nelim (bool_destruct_false_true H6) ##]
+ ##[ ##2: #H6; napply (bool_destruct ??? H6) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; nelim (bool_destruct_false_true H7) ##]
+ ##[ ##2: #H6; #H7; napply (bool_destruct ??? H7) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; nelim (bool_destruct_false_true H8) ##]
+ ##[ ##2: #H6; #H7; #H8; napply (bool_destruct ??? H8) ##]
  nletin K3 ≝ (H4 v1 v2);
  ncases (f4 v1 v2) in K3:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; #H9; nelim (bool_destruct_false_true H9) ##]
+ ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct ??? H9) ##]
  #H6; #H7; #H8; #H9; #H10;
  nrewrite > (H6 (refl_eq ??));
  nrewrite > (H7 (refl_eq ??));