The Coq mailing list

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

On 05/06/2013 11:26 AM, 
mtkhan AT risc.uni-linz.ac.at
 wrote:
> ...
> H0 : s = to_abstract_stack r /\ z = e
> ______________________________________(1/1)
> Push s z = Push (to_abstract_stack r) e
>
> my question here, how to prove structural induction reasonably
> in a well-manner in Coq.
>    

Perhaps there is some aspect of your problem that isn't expressed 
adequately by the above goal, but it looks to me like the goal can be 
proved with
    congruence
or maybe
    intuition congruence
if the former isn't smart enough.  It follows by basic properties of 
equality, with no induction required.