X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Frelations.ma;fp=matita%2Fmatita%2Flib%2Fformal_topology%2Frelations.ma;h=89273de051a3982f3825f27355f5d7ac0b52bc01;hb=bc477154d15f6979c948f9af602199af547d193e;hp=2ad35655e51756a1ceceda01182f1c126b0100f2;hpb=791b0dc201a023e772e4ba5c3da697c5ae271405;p=helm.git

diff --git a/matita/matita/lib/formal_topology/relations.ma b/matita/matita/lib/formal_topology/relations.ma
index 2ad35655e..89273de05 100644
--- a/matita/matita/lib/formal_topology/relations.ma
+++ b/matita/matita/lib/formal_topology/relations.ma
@@ -115,7 +115,7 @@ interpretation "'arrows2_REL" 'arrows2_REL A B = (arrows2 (category2_of_category
 
 
 definition full_subset: ∀s:REL. Ω^s.
- apply (λs.{x | True});
+ apply (λs.{x | ⊤});
  intros; simplify; split; intro; assumption.
 qed.
 
@@ -316,11 +316,9 @@ theorem ext_comp:
 qed.
 *)
 
-axiom daemon : False.
-
 theorem extS_singleton:
  ∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x. 
  intros; unfold extS; unfold ext; unfold singleton; simplify;
  split; intros 2; simplify; simplify in f; 
  [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
- | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.