qed.
interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+= (mk_bounded_sequence _ _ a _ _).
lemma reduce_bas_seq:
∀O:ordered_set.∀a:nat→O.∀p.∀i.