From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 1 Jul 2010 21:38:32 +0000 (+0000)
Subject: Proof simplified (??).
X-Git-Tag: make_still_working~2885
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8423682054bead9ef906bdd8c15d6e0fbd5a2194;p=helm.git

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 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.