fun (x : A -> B -> C -> ~A) => x