More re-organization.

[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 533bff3ddd2e191a8305fe229210261033d29fce..c6d91db945e94a04e325b2d33751e26022142a22 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -345,3 +345,8 @@ lemma objs2_SET1_OF_OA: OA → objs2 SET1.
  intro; whd; apply (setoid1_of_OA t);
 qed.
 coercion objs2_SET1_OF_OA.
+
+lemma Type_OF_category2_OF_SET1_OF_OA: OA → Type_OF_category2 SET1.
+ intro; apply (oa_P t);
+qed.
+coercion Type_OF_category2_OF_SET1_OF_OA.
\ No newline at end of file