The Coq mailing list

[Michael Abbott <Michael AT RCP.co.uk>]

Title: Beginner's question about induction proof

I'd like to cancel question I sent yesterday, if I may!  The question I sent is actually garbled, and I've figured out the answer to the question I meant to ask.

I meant to try and prove:
        Lemma append_assoc : (append (append f g) h) == (append f (append g h)).

and the first step, which I was missing, is:
        Generalize Y Z g h.

I do have another question about decomposing a==b, where a and b of an inductive type, into the structure of the inductive type.  I'll try and formulate this question more clearly once people are back from holidays, and once I've spent more time trying to solve it.

Regards,
        Michael Abbott