fun x: A => fun f: A -> False => f x : A -> ~~A