Merge equivalent sub-obligations instead of discarding them. (#6353)

Merge equivalent sub-obligations instead of discarding them. (#6353)

This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.