(* The only primitive data types of Matita are dependent products and universes.
So far every other user defined data type has been an inductive type. An
(* The only primitive data types of Matita are dependent products and universes.
So far every other user defined data type has been an inductive type. An