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 a1d72698ec9c91cd0b611be838d3a027fc2571c9..44f8e9f213aa2753789d4b1b83b727cdc32a4da3 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -51,17 +51,11 @@ coercion relation_pair_of_relation_pair_setoid.
 
 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;
-  [ apply (. (commute ?? r')^-1 ??);
-    apply (. H^-1 ??);
-    apply (. commute ?? r ??);
-    assumption;
-  | apply (. (commute ?? r)^-1 ??);
-    apply (. H ??);
-    apply (. commute ?? r' ??);
-    assumption;
-  ]
+ intros 5 (o1 o2 r r' H);
+ apply (.= (commute ?? r)^-1);
+ change in H with (⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
+ apply rule (.= H);
+ apply (commute ?? r').
 qed.
 
 definition id_relation_pair: ∀o:basic_pair. relation_pair o o.