]> matita.cs.unibo.it Git - helm.git/commitdiff
Some notes by Giovanni.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 26 Dec 2008 17:17:47 +0000 (17:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 26 Dec 2008 17:17:47 +0000 (17:17 +0000)
helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma

index 01eac172cebf69cdbdb416efac07d3a082e9b353..c25e44f036d613e2ebd7ed7dcdf657ec8e95955d 100644 (file)
@@ -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;