From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Jan 2010 12:49:58 +0000 (+0000)
Subject: More //.
X-Git-Tag: make_still_working~3106
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1cbf489bba32a8109f3373f43f9e3cfe2e0171f;p=helm.git

More //.
---

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 6d84ba3d8..3c7489ba3 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -48,7 +48,7 @@ ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A)
  #A; #U; #a; #H; nelim H
   [ #n; #H1; @1; nassumption
   | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
-    napply H; nnormalize; nassumption.
+    napply H; nnormalize; //.
 nqed.
 
 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
@@ -118,7 +118,7 @@ nqed.
 
 nlemma eq_rect_Type0_r:
  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); //.
 nqed.
 
 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
@@ -149,8 +149,8 @@ nlet rec cover_rect
  ncases (decide_mem … memdec b)
   [ #_; #H; napply refl; /2/
   | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
-    [ #E; napply False_rect_Type0; ncut (b=b) [//] ncases p in ⊢ (???% → ?)
-      [ #a; #K; #E2; napply H [ // | nrewrite > E2; // ]
+    [ #E; napply False_rect_Type0; ncut (b=b); //; ncases p in ⊢ (???% → ?)
+      [ #a; #K; #E2; napply H; //; nrewrite > E2; //
     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
         //]
   ##| #a; #E;
@@ -212,16 +212,13 @@ nqed.
 
 ntheorem skipfact_partial:
  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
- #n; nelim n
-  [ @1; nnormalize; @1
-  | #m; nelim m; nnormalize
-     [ #H; @2; nnormalize
-       [ //
-       | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ]
-   ##| #p; #H1; #H2; @2; nnormalize
-       [ //
-       | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
-         nrewrite < (plus_n_Sm …); // ]##]
+ #n; nelim n; /2/;
+ #m; nelim m; nnormalize
+     [ #H; @2; nnormalize; //;
+       #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
+   ##| #p; #H1; #H2; @2; nnormalize; //;
+       #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
+       nrewrite < (plus_n_Sm …); // ]
 nqed.
 
 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.