...

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
index 7fc6a07f46f0fc2f3c0bb43786a039dfc52b6d3e..2dd4147ae592f6568a644d06c713eebef6a63e7c 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
@@ -38,3 +38,21 @@ definition o_relation_pair_of_relation_pair:
     apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
     apply (orelation_of_relation_preserves_composition ?? (form BP2)  (rel BP1) ?); ]
 qed.
+
+(*
+definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 cic:/matita/formal_topology/basic_pairs/BP.con) BP).
+ constructor 1;
+  [ apply o_basic_pair_of_basic_pair;
+  | intros; constructor 1;
+     [ apply (o_relation_pair_of_relation_pair S T);
+     | intros; split; unfold o_relation_pair_of_relation_pair; simplify;
+       unfold o_basic_pair_of_basic_pair; simplify; ]
+  | simplify; intros; whd; split; unfold o_relation_pair_of_relation_pair; simplify;
+       unfold o_basic_pair_of_basic_pair;
+simplify in ⊢ (? ? ? (? % ? ?) ?);
+simplify in ⊢ (? ? ? (? ? % ?) ?);
+simplify in ⊢ (? ? ? ? (? % ? ?));
+simplify in ⊢ (? ? ? ? (? ? % ?));
+  | simplify; intros; whd; split;unfold o_relation_pair_of_relation_pair; simplify;
+       unfold o_basic_pair_of_basic_pair;simplify;
+*)
\ No newline at end of file