non-informative : Constructor arguments are in Prop only
small : Constructor arguments are not in Type and SetP and CProp
unit : Non (mutually) recursive /\ only one constructor /\ non-informative
- empty : no contructors and (in Coq) non mutually recursive
-
+ empty : in Coq: no constructors and non mutually recursive
+ in Matita: no constructors (but eventually mutually recursive
+ with non-empty types)