all pullbacks are attempted in sequence, removed many unfold

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / subsets.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index c15ef844ef169747282a61f232dbba7fd0d754d8..e6d1872166143e9f891ee27e89305a8cc0d5c658 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -145,7 +145,7 @@ definition big_intersects:
  ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
  intros; constructor 1;
   [ intro; whd; whd in I;
-    apply ({x | ∀i:I. x ∈ t i});
+    apply ({x | ∀i:I. x ∈ c i});
     simplify; intros; split; intros; [ apply (. (e^-1‡#)); | apply (. e‡#); ]
     apply f;
   | intros; split; intros 2; simplify in f ⊢ %; intro;
@@ -157,7 +157,7 @@ definition big_union:
  ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
  intros; constructor 1;
   [ intro; whd; whd in A; whd in I;
-    apply ({x | ∃i:carr I. x ∈ t i });
+    apply ({x | ∃i:I. x ∈ c i });
     simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
     [ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
     apply x;