The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

I'm reading CPDT(Certified Programming with Dependent Types) and I'm
typing all the code in the book and following through proofs. I don't
like the book's approach of using magical and non-standard proof
tactics so I'm manually proving parts that are proved using `crush`
and similar tactics.

It worked mostly fine since I already had basics grasped thanks to
SF(Software Foundations) but now I'm stuck with "dependent destruct"
parts, which I see for the first time.

I pasted the code here http://lpaste.net/107016 . I'm looking for
proving that last theorem without using magical CPDT proofs. I'd like
to go with only standard tactics/definitions. Can anyone give me some
tips on how to approach this proof? At least some keywords to do some
research would be appreciated.

Thanks.

---
Ömer Sinan Ağacan
http://osa1.net