Fix program using an the unsubstituted type of the original obligation
instead of the normalized one at the end of the proof. Fixes bug #3517.
Remove confusing behavior of unify_with_subterm that could fail with
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.