The Coq mailing list

[Stefan Monnier <monnier AT IRO.UMontreal.CA>]

>  How can one prove

>    not (eq Eq Gt)

> ?

Here's how you could write it if you don't want to use tactics (the
discriminate tactic ends up generating more or less this proof):

  Definition foo : not (eq Eq Gt) := fun P =>
    match P in eq _ gt
        return (match gt with Gt => False | _ => True end)
    with refl_equal => I
    end.

It's not exactly "obvious", but I found it is really worthwhile to try
and really understand how and why it works.


        Stefan