Full Disclosure

Bruno Barras found the following Coq proof:

fix magic (x : True) : False := magic match magic x with end
 : True -> False

This lemma is useful for getting through those troublesome proofs. Too bad it won’t be allowed in the next version of Coq.