A Mechanized Theory of Regular Trees in Dependent Type Theory