X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fbasic_pairs_to_o-basic_pairs.ma;h=2041cec40319d333f08584ac5b15571f82ee00d2;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=aee0346832275d711fc4592b13f03e7cd7147013;hpb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
index aee034683..2041cec40 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
@@ -113,10 +113,8 @@ definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP).
   | apply o_relation_pair_of_relation_pair_morphism_respects_comp;]
 qed.
 
-theorem BP_to_OBP_faithful:
- ∀S,T.∀f,g:arrows2 (category2_of_category1 BP) S T.
-   BP_to_OBP⎽⇒ f = BP_to_OBP⎽⇒ g → f=g.
- intros; change with ( (⊩) ∘ f \sub \c = (⊩) ∘ g \sub \c);
+theorem BP_to_OBP_faithful: faithful2 ?? BP_to_OBP.
+ intros 5 (S T); change with ( (⊩) ∘ f \sub \c = (⊩) ∘ g \sub \c);
  apply (POW_faithful);
  apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T));
  apply sym2;
@@ -125,9 +123,8 @@ theorem BP_to_OBP_faithful:
  apply e;
 qed.
 
-theorem BP_to_OBP_full: 
-   ∀S,T.∀f. exT22 ? (λg:arrows2 ? S T. BP_to_OBP⎽⇒ g = f).
- intros; 
+theorem BP_to_OBP_full: full2 ?? BP_to_OBP. 
+ intros 3 (S T); 
  cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
  cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);
  exists[