Some notes by Giovanni.

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index 01eac172cebf69cdbdb416efac07d3a082e9b353..c25e44f036d613e2ebd7ed7dcdf657ec8e95955d 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -60,6 +60,7 @@ definition relation_pair_equality:
   ]      
 qed.
 
+(* qui setoid1 e' giusto *)
 definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
  intros;
  constructor 1;