X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=54e9d98f0c30a07472c19bca4fba55e44e99d535;hb=0881f6e27c5bb3434e967f4d966465c576146a6e;hp=7a52e5f064260f1a9f04463a4414e8b0c7b6962a;hpb=c231702a57076acf0c161cdb4799bf83158175f0;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 7a52e5f06..54e9d98f0 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -350,15 +350,15 @@ notation "'segment_preserves_infimum'" non associative with precedence 90 for @{
 interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
 interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
 
-(* TEST, ma quanto godo! *)
-lemma segment_preserves_infimum2:
+(*
+test segment_preserves_infimum2:
   ∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}. 
     ⌊n,\fst (a n)⌋ is_decreasing ∧ 
     (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
 intros; apply (segment_preserves_infimum s a x H);
 qed.
 *)
-           
+       
 (* Definition 2.10 *)
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
@@ -394,8 +394,8 @@ interpretation "Ordered set lower locatedness" 'lower_located s =
 lemma h_uparrow_upperlocated:
   ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
-cases H3 (H4 H5); clear H3; cases (hos_cotransitive ??? u Hxy) (W W);
-[2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
+cases H3 (H4 H5); clear H3; cases (hos_cotransitive C y x u Hxy) (W W);
+[2: cases (H5 x W) (w Hw); left; exists [apply w] assumption;
 |1: right; exists [apply u]; split; [apply W|apply H4]]
 qed.