1) Some reorganization.

[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 058176f4ce4556e07a5d10dc08049f05d59948c9..97e386c1545e1b3b8af6122a94843f7ed2e418ef 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -185,27 +185,3 @@ qed.
 interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
 *)
-
-include "o-basic_pairs.ma".
-(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair.
- intro;
- constructor 1;
-  [ apply (SUBSETS (concr b));
-  | apply (SUBSETS (form b));
-  | apply (orelation_of_relation ?? (rel b)); ]
-qed.
-
-definition o_relation_pair_of_relation_pair:
- ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 →
-  relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
- intros;
- constructor 1;
-  [ apply (orelation_of_relation ?? (r \sub \c));
-  | apply (orelation_of_relation ?? (r \sub \f));
-  | lapply (commute ?? r);
-    lapply (orelation_of_relation_preserves_equality ???? Hletin);
-    apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1);
-    apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
-    apply (orelation_of_relation_preserves_composition ?? (form BP2)  (rel BP1) ?); ]
-qed.
\ No newline at end of file