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