include "excess.ma".
-definition sequence := λO:excess.nat → O.
+definition sequence := λO:Type.nat → O.
-definition fun_of_sequence: ∀O:excess.sequence O → nat → O ≝ λO.λx:sequence O.x.
+definition fun_of_sequence: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.x.
coercion cic:/matita/sequence/fun_of_sequence.con 1.