Actually, I had expected that the first rule works. I need to dig into this again. The rule that should definitely work is the followingNo, it doesn't. This produces the same effect like the congruence rule "[| M = N; f M = g N |] ==> Let M f = Let N g", it produces too many induction hypotheses."f M = g N ==> Let M f = Let N g"It has the same effect on the induction rule as unfolding all lets. Can you try if it works for your function?
After playing the complete example that you provided off-list, I think I now understood the problem.
The let binding itself contains recursive calls. Using the above congruence rule is equivalent to inlining all lets for the purpose of the analysis. This automatically duplicates recursive calls, if the let-bound variable occurs more than once. I think there is no way to avoid this using congruence rules.
The transformation you would like to see could in fact be done as a post-processing step on the induction rule. Would you (and other users) think it is a good idea to inline assumptions of the form "x = t" in general?