(* *)
(**************************************************************************)
-include "uniform.ma".
+include "dama/uniform.ma".
record ordered_uniform_space_ : Type ≝ {
ous_os:> ordered_set;
change in H1:(? ? ? %) with (\fst b);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
- apply rule H1;
+ apply rule (x2sx_ ? s ?? H1);
| right; change in H1:(? ? % ?) with (\fst b);
change in H1:(? ? ? %) with (\fst a);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
- apply rule H1;]
+ apply rule (x2sx_ ? s ?? H1);]
qed.