ordered_set simplified

[helm.git] / helm / software / matita / contribs / dama / dama / nat_ordered_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index dfeaa6d35074c8cddc99f7798a332ba8bdc21b66..26e2f0d2953a75ac9e3706babd7ec22a3b4f695d 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -44,11 +44,10 @@ cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
 qed.
   
 lemma nat_ordered_set : ordered_set.
-letin hos ≝ (mk_half_ordered_set nat (λT:Type.λf:T→T→CProp.f) ? nat_excess ? nat_excess_cotransitive);
+letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
 [ intros; left; intros; reflexivity;
 | intro x; intro H; apply (not_le_Sn_n ? H);]
-constructor 1;  
-[ apply hos; | apply (dual_hos hos); | reflexivity]
+constructor 1;  apply hos;
 qed.
 
 interpretation "ordered set N" 'N = nat_ordered_set.