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.

2006-12-11T20:35:00Z

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.