[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)

[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)

Previously the trivial cycle check only covered the case in which the currently-being-expanded assumption `A` had as its stored proof node `pf` an assumption proof justifying itself. However, it can be the case that `pf` is not an assumption proof, but a proof that nevertheless has `A` as one of its free assumptions. This commit generalizes the trivial cycle check to account for this.