The new coercion from SET to Type0 with higher priority really helps a lot:

[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..eaa6954a4c5137eb69fb3a3c9d77923b4f42610b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -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 ∈ t i });
     simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
     [ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
     apply x;