Hola Pablo.
El término fun (A:Set) (x:A) (y:A) => x tendría tipo forall A:Set, A -> A -> A y no: forall A:Set, A -> A.
En realidad el tipo más general de este operador (K) podría tener dos Sets diferentes (A y B) y el término sería:
fun (A B:Set) (x:A) (y:B) => x
con tipo forall A B:Set, A -> B -> A
Saludos, Carlos