The invariant holds in every reachable state.
Theorem: unequivocal-dags-p-when-reachable
(defthm unequivocal-dags-p-when-reachable (implies (and (system-state-reachablep systate) (system-committees-fault-tolerant-p systate)) (unequivocal-dags-p systate)))
