def x : Set = Set ;

def x : (A:Set) -> A = x