Invariant that the previous certificates of every certificate in every DAG form a quorum if the round is not 1, and there are none in round 1.
This is a specialization of invariant-previous-are-quorum, which applies to all certificates in the system; the specialization only applies to DAGs. This specialized invariant is formulated in a way that is useful to prove further properties.
This specialized invariant is expressed in terms of the dag-previous-are-quorum-p predicate, which is used in further proofs of correctness properties.