notation made half decent

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 310ef55ebf53f23dbd552cda169685204ec5b17b..b3e69b09cf7afcaf038d7d95b379011de6d05e19 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -86,7 +86,7 @@ intro; split; intro; simplify; intro;
   clear Hletin Hletin1; cases Hletin2; whd in x2; 
 qed.
 *)
-lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+lemma curry: ∀A,B,C.(A × B ⇒_1 C) → A → (B ⇒_1 C).
  intros;
  constructor 1;
   [ apply (b c);
@@ -96,8 +96,8 @@ qed.
 notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
 interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
 
-definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
-intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) =_1 ?);
 constructor 1; constructor 1;
 [ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
   apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});