Can coq express its own metatheory?

Question

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?