all pullbacks are attempted in sequence, removed many unfold

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index 74a7c7d7839bb26fee44529654fc3cc5ff653bb2..307797566dce8ea8280697246208f44e943a6fbf 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -98,10 +98,8 @@ definition REL: category1.
           first [apply refl | assumption]]]
 qed.
 
-(* 
 definition setoid_of_REL : objs1 REL → setoid ≝ λx.x.
 coercion setoid_of_REL.
-*)
 
 definition binary_relation_setoid_of_arrow1_REL : 
   ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x.