some notation for map_arrows2

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_pairs.ma

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..8e5421c1f0b39617a9896c045a7070b64c606061 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.
@@ -178,6 +172,7 @@ definition relation_pair_setoid_of_arrows1_BP :
   ∀P,Q. arrows1 BP P Q → relation_pair_setoid P Q ≝ λP,Q,x.x.
 coercion relation_pair_setoid_of_arrows1_BP.
 
+(*
 definition BPext: ∀o: BP. (form o) ⇒_1 Ω^(concr o).
  intros; constructor 1;
   [ apply (ext ? ? (rel o));
@@ -225,3 +220,4 @@ qed.
 
 interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr ?) ?? (relS c) x y).
 interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ??? (relS c)).
+*)