- new notation.ma file with local and common notation

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations_to_o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 2368affe0fca9711d74ff0395518b28483f10a4b..b3939f90ba68dfd1f1fa57eed6e8003d322f21e9 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -182,10 +182,8 @@ theorem SUBSETS_faithful:
   |*: cases Hletin1; cases x1; change in f3 with (eq1 ? x w); apply (. f3‡#); assumption;]
 qed.
 
-inductive exT2 (A:Type2) (P:A→CProp2) : CProp2 ≝
-  ex_introT2: ∀w:A. P w → exT2 A P.
 
-theorem SUBSETS_full: ∀S,T.∀f. exT2 ? (λg. map_arrows2 ?? SUBSETS' S T g = f).
+theorem SUBSETS_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? SUBSETS' S T g = f).
  intros; exists;
   [ constructor 1; constructor 1;
      [ apply (λx:carr S.λy:carr T. y ∈ f (singleton S x));