+lemma hint1:
+ ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
+ → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set l u))).
+intros; assumption;
+qed.
+
+coercion hint1 nocomposites.
+
+alias symbol "pi1" = "exT \fst".
+alias symbol "N" = "ordered set N".