From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jan 2010 16:15:09 +0000 (+0000)
Subject: We are still equivalent (even if the definition of ncover is obfuscated).
X-Git-Tag: make_still_working~3122
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8b33918a53a2c752e2256b328bc0e45f4827beac;p=helm.git

We are still equivalent (even if the definition of ncover is obfuscated).
---

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 40378c07b..32d0f8f84 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -39,22 +39,22 @@ ninductive ncover (A : nAx) (U : Ω^A) : A → CProp[0] ≝
 
 interpretation "ncovers" 'covers a U = (ncover ? U a).
 
-(*XXX
 ntheorem ncover_cover_ok: ∀A:nAx.∀U.∀a:A. a ◃ U → cover (Ax_of_nAx A) U a.
  #A; #U; #a; #H; nelim H
   [ #n; #H1; @1; nassumption
   | #a; #i; #IH; #H; @2 [ napply i ]
     nnormalize; #y; *; #j; #E; nrewrite > E;
-    napply H ]
+    napply H;
+    /2/ ]
 nqed.
 
 ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A) U a.
  #A; #U; #a; #H; nelim H
   [ #n; #H1; @1; nassumption
-  | #a; #i; #IH; #H; @2 [ napply i ] #j; ncases j; #x; #K;
+  | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
     napply H; nnormalize; nassumption.
 nqed.
-*)
+
 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 
 interpretation "ncoverage cover" 'coverage U = (ncoverage ? U).