Theorem: vl-depgraph-p-of-invert
(defthm vl-depgraph-p-of-invert (implies (vl-depgraph-p x) (vl-depgraph-p (depgraph::invert x))))