blob: d96c1e8f96c2e5cd6f8dbde1d17077575c7f5c09 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* Check that the encoding of system U- fails *)
Require Hurkens.
Inductive prop : Prop := down : Prop -> prop.
(* Coq should reject the following access of a Prop buried inside
a prop. *)
Definition up (p:prop) : Prop := let (A) := p in A.
(* Otherwise, we would have a proof of False via Hurkens' paradox *)
Definition paradox : False :=
Hurkens.NoRetractFromSmallPropositionToProp.paradox
prop
down
up
(fun (A:Prop) (x:up (down A)) => (x:A))
(fun (A:Prop) (x:A) => (x:up (down A)))
False.
|