nat model ported to the dualized version, but not itself dualized dedekind-sig-compl...

[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_order_continuous.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
index b8e23cc38beaf9f6a3e2f936fc5d806676582476..7949ba2d28714d077a1f5976b58af8b73f351276 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
@@ -25,7 +25,7 @@ intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
     generalize in match (refl_eq ? (a i):a i = a i);
     generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;  
     intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
-    apply (us_phi1 nat_uniform_space ? H3); simplify; apply eq_reflexive;
+    apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));
 |2: cases (nat_dedekind_sigma_complete_r l u a H1 ? H2); 
     exists [apply w1]; intros; 
     apply (restrict nat_ordered_uniform_space l u ??? H4);     
@@ -34,6 +34,6 @@ intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
     generalize in match (refl_eq ? (a i):a i = a i);
     generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;  
     intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
-    apply (us_phi1 nat_uniform_space ? H3); simplify; apply eq_reflexive;]
+    apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));]
 qed.