Add `Theory::explain_propagation_final` for use in `analyze_final`

[dewert99]

This allows theories to produce different explanations in analyze, and analyze_final. For example, if a theory knows (a && b) => c and c => d and is asked to explain d, it may prefer to explain using [c] in analyze to generate a better clause, but may as well explain using [a, b] in analyze_final since otherwise it would just be asked to explain c anyway.