The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

I don't see the point. If you are worried about people playing syntactic 
games,
examine the statement with notations and coercions turned off. You
might as well say you have a "contradiction" because you can write

Notation "'Truth'" := False.

Lemma contradiction : Truth -> False. auto. Qed.

"t" isn't a sort, so it's obvious your goal won't typecheck without
coercions. Displaying coercions, you have

exists a : t, exp2 a -> False.

We see exp2 = (fun _ => False), so this should be equivalent to
exists a : t, (fun _ => False) a -> False.

Unfolding exp2 gives

ex _ (fun _ : True => False -> False).

And there's nothing wrong with being able to prove that.

Brandon