From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Jan 2009 14:10:51 +0000 (+0000)
Subject: The functor from BP to OBP has been defined (but no property proved yet).
X-Git-Tag: make_still_working~4280
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dba85ad7c7510e7bfd01e5721c63dad528b3e0bf;p=helm.git

The functor from BP to OBP has been defined (but no property proved yet).
---

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 071892f6b..058176f4c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -203,6 +203,9 @@ definition o_relation_pair_of_relation_pair:
  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