The Coq mailing list

[t x <txrev319 AT gmail.com>]

EDIT: last line is meant to be "induction expr; auto" not "destruct expr; auto"

On Sun, Aug 18, 2013 at 4:09 PM, t x <txrev319 AT gmail.com> wrote:

Hi,

  Can someone post a minimal solution to this (without using dep_destruct from cpdt tactics) ?

  https://gist.github.com/anonymous/6262395

  Proofs involving dependent types seems to high levels of "black magic" which makes it nearly impossible to debug. I'd like to see a minimal "manual" solution to see what's going on.

Thanks