Constructor subtyping in the Calculus of Inductive Constructions

The Calculus of Inductive Constructions (CIC) is a powerful type system, featuring dependent types and inductive definitions, that forms the basis of proof-assistant systems such as Coq and Lego. We extend CIC with constructor subtyping, a basic form of subtyping in which an inductive type A is viewed as a subtype of another inductive type B if B has more elements than A. It is shown that the calculus is well-behaved and provides a suitable basis for formalizing natural semantics in proof-development systems.