blob: ad4941084cf7969ec4df3a6b4f4df06dd7ecb345 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import ProofIrrelevance.
Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2.
exact proof_irrelevance.
Qed.
Lemma paradox : False.
assert (H : 0 <> 1) by discriminate.
apply H.
Fail apply proof_irrelevance. (* inlined version is rejected *)
apply proof_irrelevance_set.
Qed.
|
