added some virtuals

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 4c61f0fb47753fc191b383a9f74bff27c0d718de..0cb3fe1172a341f7ac5fe1ba53530c7d5d13adff 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -26,11 +26,6 @@ constructor 1; [apply bool] constructor 1;
   try assumption; apply I]
 qed.
 
-definition setoid_OF_SET: objs1 SET → setoid.
- intros; apply o; qed.
-
-coercion setoid_OF_SET.
-
 lemma IF_THEN_ELSE_p :
   ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → 
     (λm.match m with [ true ⇒ a | false ⇒ b ]) x =
@@ -297,4 +292,4 @@ split;
    | apply ((comp_assoc1 ????? H* G* F* ));]
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1;
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;]
-qed.
\ No newline at end of file
+qed.