Fallback for sequential substitution proof reconstruction (#8730)
This makes our proof reconstruction fallback to a trivial sequential reconstruction in very rare cases where a sequential substitution fails to reconstruct. This can happen in some rare cases where terms are used in the domain of a substitution that otherwise would be modified by earlier substitutions. This occurs on 2 QF_SLIA benchmarks, attached is a delta-debugged version.
This also changes a warning message to a trace for this case, as a warning message may cause LFSC proof checking to fail when it should just give a warning for a TRUST_SUBS step, which is the default behavior regardless.