X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-algebra.ma;h=533bff3ddd2e191a8305fe229210261033d29fce;hb=bb0fff7ebc68535a75e260082b7db26c1d99f643;hp=029e93258b8cdf010dafa3e94c722fd5e7933b5b;hpb=1c406089d385be2d444308a783bc051bd28be463;p=helm.git

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 029e93258..533bff3dd 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -335,3 +335,13 @@ lemma setoid1_of_OA: OA → setoid1.
  intro; apply (oa_P t);
 qed.
 coercion setoid1_of_OA.
+
+lemma SET1_of_OA: OA → SET1.
+ intro; whd; apply (setoid1_of_OA t);
+qed.
+coercion SET1_of_OA.
+
+lemma objs2_SET1_OF_OA: OA → objs2 SET1.
+ intro; whd; apply (setoid1_of_OA t);
+qed.
+coercion objs2_SET1_OF_OA.