X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs.ma;h=a1d72698ec9c91cd0b611be838d3a027fc2571c9;hb=8423682054bead9ef906bdd8c15d6e0fbd5a2194;hp=0734411f8d07192881bcb29516b089959d80f2d8;hpb=7ce86e8bd53bef149ed427cf036c3ae0c6ef0486;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index 0734411f8..a1d72698e 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -53,12 +53,14 @@ lemma eq_to_eq':
   ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
  intros 7 (o1 o2 r r' H c1 f2);
  split; intro H1;
-  [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
-    lapply (if ?? (H c1 f2) H2) as H3;
-    apply (if ?? (commute ?? r' c1 f2) H3);
-  | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2;
-    lapply (fi ?? (H c1 f2) H2) as H3;
-    apply (if ?? (commute ?? r c1 f2) H3);
+  [ apply (. (commute ?? r')^-1 ??);
+    apply (. H^-1 ??);
+    apply (. commute ?? r ??);
+    assumption;
+  | apply (. (commute ?? r)^-1 ??);
+    apply (. H ??);
+    apply (. commute ?? r' ??);
+    assumption;
   ]
 qed.