We present a “destruct” tactic that supports dependent types written in Mtac2. The tactic is implemented to a large degree in Coq itself — only using Mtac2’s unsafe features when absolutely necessary. To this end, the development includes fully-typed descriptions of 1) inductive datatypes, 2) arguments of inductive datatypes, 3) constructors of inductive dataypes, 4) branches of matches on values of inductive datatypes, and 5) return types of matches on values of inductive datatypes. Additionally, we also propose a way of dealing with meta-programs that are parametric in Prop/Type.