On principal types and well-foundedness of terms in ECC

When we investigate a type system, it is helpful if we can establish the well-foundedness of types or terms with respect to a certain hierarchy, and the Extended Calculus of Constructions (called ECC, defined and studied comprehensively in [Luo, 1994]) is no exception. However, under a very natural hierarchy relation, the well-foundedness of terms does not hold generally. In this article, the well-foundedness are established for two natural families of terms (namely, types in a valid context and terms having normal forms). Also, we give an independent proof of the existence of principal types in ECC since it is used in the proof of well-foundedness of types in a valid context although it is often proved by utilizing the well-foundedness of terms, which would make our argument circular if adopted.