1) no more DAEMONS

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-concrete_spaces.ma

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 4e989cb14f6489c02bb5d9330354e33292ad4b55..61b8f77e7582b2b0f4834537d63d1ab7909b3dc2 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
@@ -32,15 +32,20 @@ notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}
 interpretation "Existential pre-image ⊩⎻" 'ext x = (or_f_minus _ _ (rel x)).
 
 definition A : ∀b:BP. unary_morphism (oa_P (form b)) (oa_P (form b)).
-intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); | intros; apply (†(†H));] qed. 
+intros; constructor 1;
+ [ apply (λx.□_b (Ext⎽b x));
+ | do 2 unfold FunClass_1_OF_carr1; intros; apply  (†(†H));]
+qed.
 
 lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed.
 coercion xxx.
 
 definition d_p_i : 
-  ∀S:setoid.∀I:setoid.∀d:unary_morphism S S.∀p:ums I S.ums I S.
-intros; constructor 1; [ apply (λi:I. u (c i));| intros; apply (†(†H));].
-qed. 
+  ∀S,I:SET.∀d:unary_morphism S S.∀p:arrows1 SET I S.arrows1 SET I S.
+intros; constructor 1;
+ [ apply (λi:I. u (c i));
+ | unfold FunClass_1_OF_carr1; intros; apply (†(†H));].
+qed.
 
 alias symbol "eq" = "setoid eq".
 alias symbol "and" = "o-algebra binary meet".