freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
index 3726219a8c02a6002edbbddb64db2b0ed3a12217..e6be57877ae3b5f6d799dbd9b05d9b1367edea0a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
@@ -30,7 +30,7 @@ include "freescale/exadecim.ma".
 ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -39,7 +39,7 @@ nqed.
 ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -48,7 +48,7 @@ nqed.
 ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -57,7 +57,7 @@ nqed.
 ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -66,7 +66,7 @@ nqed.
 ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##5: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -75,7 +75,7 @@ nqed.
 ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##6: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -84,7 +84,7 @@ nqed.
 ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##7: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -93,7 +93,7 @@ nqed.
 ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##8: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -102,7 +102,7 @@ nqed.
 ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##9: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -111,7 +111,7 @@ nqed.
 ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##10: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -120,7 +120,7 @@ nqed.
 ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##11: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -129,7 +129,7 @@ nqed.
 ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##12: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -138,7 +138,7 @@ nqed.
 ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##13: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -147,7 +147,7 @@ nqed.
 ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##14: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -156,7 +156,7 @@ nqed.
 ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##15: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]
@@ -165,7 +165,7 @@ nqed.
 ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
  #e2; #P; ncases e2; nnormalize; #H;
  ##[ ##16: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
           nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
           nrewrite > H; nnormalize; napply I
  ##]