The Coq mailing list

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

On 10/22/2013 09:57 AM, t x wrote:
> Is https://gist.github.com/anonymous/7100956 correct?
> Where error (1) is fixed at line 18 and error (2) is fixed at line 21.

No, there are still issues.
- You can't just write "typeof(Di)"; it's necessary to extend the typing 
context with variables "y*_*" of appropriate types.
- On the same line, you substitute "u_i" for "x_i", which can't be 
right, because "u_i" is independent of which pattern has matched.  You 
need to use the type of "Cn" to figure out the right terms to substitute.