From 8b33918a53a2c752e2256b328bc0e45f4827beac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Jan 2010 16:15:09 +0000 Subject: [PATCH] We are still equivalent (even if the definition of ncover is obfuscated). --- helm/software/matita/nlibrary/topology/igft3.ma | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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). -- 2.39.2