[proof-new] Catch trivial cycles in SAT proof generation (#5853)

[proof-new] Catch trivial cycles in SAT proof generation (#5853)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from

       l1 v l2   ~l1 v l3   ~l2 v l3
(ok) ------------------------------
                  l3
in which l3 = l1 v l2, to

         l1 v l2   ~l1 v l3   ~l2 v l3
(bad) ------------------------------
               l3 v l3
              ---------
                 l3
This commit now catches the trivial cycle before it's generated.