The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Dear Coq-developers,

On tuesday we realized that there is a much shorter proof of PE -> PI then the one given in the standard library (http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html#), following the following two steps:

1. PE -> forall X:Prop, X -> X = True
2. (forall X:Prop, X -> X = True) -> PI

One elegant formalization is as follows:

Goal prop_extensionality -> proof_irrelevance.
intros D X E F.
assert (C: X=True) by intuition.
subst. destruct E, F. reflexivity.
Qed.

Why does the standard library include the other proof over this one?

Kind regards,

jonas