The Coq mailing list

[andré hirschowitz <ah AT unice.fr>]

This could probably be simplified into

False * True <-> False <-> False * False.

ah 

2012/8/4 Vladimir Voevodsky <vladimir AT ias.edu>

This is not provable. In fact in combination with propositional extensionality (axiom saying that for A,B:Prop one has (A<->B)->(A=B ) it would imply the excluded middle.

Indeed, for all A:Prop, (A or (not A) is nonempty and on the other hand

((A or (not A)) and True)  <->  (A or (not A) )  <-> ((A or (not A)) and (A or (not A)))