Proof simplified (??).

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 0734411f8d07192881bcb29516b089959d80f2d8..a1d72698ec9c91cd0b611be838d3a027fc2571c9 100644 (file)
--- 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.