X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_pairs.ma;h=c25e44f036d613e2ebd7ed7dcdf657ec8e95955d;hb=06585b97fad3158391dbbea1fcad5866f5269eee;hp=9bd76ebeb78a45fb6ff3977a6080c1ea013b04f6;hpb=62e9e8296d172d6497f9ad29bad402fbad2014c3;p=helm.git

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 9bd76ebeb..c25e44f03 100644
--- 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;
@@ -70,7 +71,7 @@ qed.
 
 lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
  intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c);
- apply (.= (commute ?? r \sup -1));
+ apply (.= ((commute ?? r) \sup -1));
  apply (.= H);
  apply (.= (commute ?? r'));
  apply refl1;