Concrete Spaces defined but... they require about 20m to type-check!

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index c3221a7d99a0068e52b17781c8be2aa01ece8afd..80ee4649fee1f149370a456e5c81d28f9375d26e 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -129,12 +129,12 @@ definition convergent_relation_space_composition:
  ∀o1,o2,o3: concrete_space.
   binary_morphism1
    (convergent_relation_space_setoid o1 o2)
-   (convergent_relation_space_setoid o2 o3)
+   (convergentin ⊢ (? (? ? ? (? ? ? (? ? ? ? ? (? ? ? (? ? ? (% ? ?))) ?)) ?) ? ? ?)_relation_space_setoid o2 o3)
    (convergent_relation_space_setoid o1 o3).
  intros; constructor 1;
      [ intros; whd in c c1 ⊢ %;
        constructor 1;
-        [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+        [ apply (c1 ∘ c);
         | intros;  
           change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
           alias symbol "trans" = "trans1".
@@ -158,25 +158,16 @@ definition CSPA: category1.
   | apply convergent_relation_space_setoid
   | intro; constructor 1;
      [ apply id1
-     | intros;
-       unfold id; simplify;
-       apply (.= (equalset_extS_id_X_X ??));
-       apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
-                    (equalset_extS_id_X_X ??)\sup -1)));
-       apply refl1;
-     | apply (.= (equalset_extS_id_X_X ??));
-       apply refl1]
+     | intros; apply refl1;
+     | apply refl1]
   | apply convergent_relation_space_composition
   | intros; simplify;
     change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
-    apply (.= ASSOC1);
-    apply refl1
+    apply ASSOC1;
   | intros; simplify;
     change with (a ∘ id1 ? o1 = a);
-    apply (.= id_neutral_right1 ????);
-    apply refl1
+    apply (id_neutral_right1 : ?);
   | intros; simplify;
     change with (id1 ? o2 ∘ a = a);
-    apply (.= id_neutral_left1 ????);
-    apply refl1]
-qed.
+    apply (id_neutral_left1 : ?);]
+qed.
\ No newline at end of file