[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

The justifications for the theory lemmas (i.e., THEORY_LEMMA steps) sometimes was not being properly connected with the actual clause inserted into the SAT solver, leading to open proofs. The issue was triggered by a regression being added in ##8819, so we don't need to add one here.