freescale porting, work in progress

[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 02bd4e1384cafeec5c116a5301ef0c93b4e12886..d6995ec0be5526c24e100f9d0353c0eeacf91f32 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,9 +54,9 @@ nlemma symmetric_eqpair :
  (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;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
  #x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
  #x2; #y2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -74,9 +74,9 @@ nlemma eq_to_eqpair :
  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
  (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
  #x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
  #x2; #y2; #H;
  nnormalize;
  nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
@@ -92,9 +92,9 @@ nlemma eqpair_to_eq :
  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
  (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
  #x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
  #x2; #y2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
@@ -146,9 +146,9 @@ nlemma symmetric_eqtriple :
  (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;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
  #x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
  #x2; #y2; #z2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -172,9 +172,9 @@ nlemma eq_to_eqtriple :
  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
  (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
  #x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #H;
  nnormalize;
  nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
@@ -193,9 +193,9 @@ nlemma eqtriple_to_eq :
  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
  #x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
@@ -262,9 +262,9 @@ nlemma symmetric_eqquadruple :
  (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;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -294,9 +294,9 @@ nlemma eq_to_eqquadruple :
  (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
  (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #H;
  nnormalize;
  nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
@@ -318,9 +318,9 @@ nlemma eqquadruple_to_eq :
  (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);
@@ -403,9 +403,9 @@ nlemma symmetric_eqquintuple :
  (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;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #w2;
  nnormalize;
  nrewrite > (H x1 x2);
@@ -441,9 +441,9 @@ nlemma eq_to_eqquintuple :
  (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
  (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #w2; #H;
  nnormalize;
  nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
@@ -468,9 +468,9 @@ nlemma eqquintuple_to_eq :
  (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
  #x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
  #x2; #y2; #z2; #v2; #w2; #H;
  nnormalize in H:(%);
  nletin K ≝ (H1 x1 x2);