I'm learning about language metatheory and type systems, and am using coq to formalize my study.  One of the things I'd like to do is examine type systems that include dependent types, which I understand is very involved: being able to rely on coq would be invaluable.Since this type system feature (and other, simpler ones) brings the expressive power of my studied system closer to coq's own, I worry that I might run into a bootstrapping problem that might not reveal itself until much later.  Perhaps someone here can address my fears before I set out.Can coq express its own metatheory?  If not, can it still express simpler systems that include common forms of dependent typing?
Can coq express its own metatheory?
type theory;dependent types;coq
It is possible to formalize Coq's logic within Coq but only subsets of the logic have been formalized yet. Relevant contributions are CoqInCoq, PTS, PTSATR, and PTSF.