X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft2.ma;h=4703fba8c770659fc251fe5f0cf689e3a1f64653;hb=0846ed20135a60c0230d38d07fc2e78ff7a1e9b9;hp=1232642d8b03a816fe6cdae913225424a6709884;hpb=bf156ee614529e006190285801e1c7b499cbe029;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 1232642d8..4703fba8c 100644
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -14,6 +14,10 @@
 
 include "topology/igft.ma".
 
+nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
+nnormalize; nauto;
+nqed.
+
 alias symbol "covers" = "covers set".
 alias symbol "coverage" = "coverage cover".
 alias symbol "I" = "I".
@@ -22,7 +26,8 @@ nlemma cover_ind':
    (U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a j ⊆ P → a ∈ P) →
     ◃ U ⊆ P.
  #A; #U; #P; #refl; #infty; #a; #H; nelim H
-  [ nauto | #b; #j; #K1; #K2; napply (infty … j) [ nassumption | napply K2]##]
+  [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2; 
+            napply infty; nauto; ##] 
 nqed.
 
 alias symbol "covers" = "covers".
@@ -30,6 +35,7 @@ alias symbol "covers" = "covers set".
 alias symbol "covers" = "covers".
 alias symbol "covers" = "covers set".
 alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
 nlemma cover_ind'':
  ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
   (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
@@ -70,7 +76,7 @@ ncoercion uuax : ∀u:uuAx. Ax ≝ uuax on _u : uuAx to Ax.
 
 nlemma eq_rect_Type0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+ #A; #a; #x; #p; ncases p; nauto;
 nqed.
 
 nlemma eq_rect_Type0_r:
@@ -92,6 +98,8 @@ nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
 
 alias symbol "covers" = "covers".
 alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+alias symbol "covers" = "covers set".
 nlet rec cover_rect
  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
   (refl: ∀a:uuax A. a ∈ U → P a)
@@ -114,7 +122,8 @@ nlet rec cover_rect
             nrewrite > E2; nnormalize; #_; nauto]##]
       #Hcut; 
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
-      napply (H2 one); #y; #E2; nrewrite > E2
+      napply (H2 one); #y; #E2; nrewrite > E2 
+      (* [##2: napply cover_rect] nauto depth=1; *)
        [ napply Hcut
-     ##| napply (cover_rect A U memdec P refl infty a); napply Hcut]##]
+     ##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
 nqed.
\ No newline at end of file