The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/07/2013 06:35 AM, 
mtkhan AT risc.uni-linz.ac.at
 wrote:
> Thanks for the reply. However, I am interested in the general
> proof strategy of Coq regarding the proofs which involve
> structural equality.
>    

It really is true that [congruence] will prove all such equalities, 
after you perform problem-specific simplifications in your goal.