1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Check that arguments of impredicative types are not considered
subterms even through commutative cuts on functional arguments
(example prepared by Bruno) *)
Inductive IMP : Prop :=
CIMP : (forall A:Prop, A->A) -> IMP
| LIMP : (nat->IMP)->IMP.
Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))).
Definition Paradox : False :=
(fix F y o {struct o} : False :=
match y with
| tt => fun f =>
match f 0 with
| CIMP h => F y (h _ o)
| _ => F y (f 0)
end
end match o with LIMP f => f | _ => fun _ => o end) tt i0.
|
