The Coq mailing list

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

On 12/29/2012 02:37 PM, 
abc.deaf.xyz AT gmail.com
 wrote:
> I want to write it as follows:
>
>      Theorem nope n (p : n = O) (q : n<>  O) : False.
>        contradict q.
>        exact p.
>      Qed.
>
>      Definition pred2 n (q : n<>  O) :=
>        match n with
>          | S n =>  n
>          | O   =>
>            let p := _ in
>            match nope n p q with end
>        end.
>
> My problem is... what do I fill in the hole in the let clause?
>    

I actually treat the example of dependently typed predecessor at length 
in Chapter 6 of CPDT <http://adam.chlipala.net/cpdt/>.  The version 
you're looking for is one among several that the chapter works its way 
through.