Invariant that all the certificate in a DAG at least two rounds after the last committed anchor of a possibly different DAG have paths to that anchor in the first DAG.
This is a very fundamental and critical invariant of the protocol. It generalizes invariant-paths-to-last-anchor, by considering two DAGs in two validators, which logically means that they could be the same DAG and validator or not. So in fact this invariant subsumes that invariant, but for now we prefer to keep that invariant around, also because it is a bit simpler to understand and prove.
This invariant is implied by other already proved invariants, which establish the (suitably instantiated) hypothesis of dag-all-path-to-p-other-holds, so that it can be applied to the DAGs of the two validators. See property-paths-to-other-voted-anchor for an explanation of this invariant/property.