No more daemons, no more exTs.

[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 6351fead91eca85d504ca36b96a93d70a4153db2..41e29a4fb8ff756dd0ea0f00620d5a39b1fcd063 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -153,15 +153,11 @@ definition big_intersects:
      | apply (. (#‡(e i)\sup -1)); apply f]]
 qed.
 
-(* senza questo exT "fresco", universe inconsistency *)
-inductive exT (A:Type0) (P:A→CProp0) : CProp0 ≝
-  ex_introT: ∀w:A. P w → exT A P.
-
 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*) exT (carr I) (λi. x ∈ t i)});
+    apply ({x | ∃i:carr I. x ∈ t i });
     simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
     [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
     apply x;