∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
intros; cases H (Ha Hx); split;
∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
intros; cases H (Ha Hx); split;