2 lines
48 B
Plaintext
2 lines
48 B
Plaintext
fun x: A => fun f: A -> False => f x : A -> ~~A
|
fun x: A => fun f: A -> False => f x : A -> ~~A
|