-definition hint_sequence:
- ∀C:ordered_set.
- sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
-intros;assumption;
-qed.
-
-definition hint_sequence1:
- ∀C:ordered_set.
- sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C).
-intros;assumption;
-qed.
-
-definition hint_sequence2:
- ∀C:ordered_set.
- sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)).
-intros;assumption;
-qed.
-
-definition hint_sequence3:
- ∀C:ordered_set.
- sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)).
-intros;assumption;
-qed.
-
-coercion hint_sequence nocomposites.
-coercion hint_sequence1 nocomposites.
-coercion hint_sequence2 nocomposites.
-coercion hint_sequence3 nocomposites.
-