aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/prop-set-proof-irrelevance.v
blob: fee33432b0b082d4a8a1de02b5d25d87ad7a1d47 (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.
  Fail 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.*)