more notation

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

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 aee0346832275d711fc4592b13f03e7cd7147013..2041cec40319d333f08584ac5b15571f82ee00d2 100644 (file)
--- 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[