some more if/fi conversion due to the new . binding

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index 324e51df7a2fcc651b0af478255db26f1364ab6a..2ee78912afa42af75a8874e3244e5b43090a435b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -18,7 +18,7 @@ include "o-basic_topologies.ma".
 lemma pippo: ∀S:OA.∀p,q,r:S. p ≤ q → p >< r → q >< r.
  intros;
  cut (r = binary_meet ? r r); (* la notazione non va ??? *)
-  [ apply (. (#‡Hcut) ^ -1);
+  [ apply (. (#‡Hcut));
     apply oa_overlap_preservers_meet;
   | 
   ]