def id : (A:Set) -> (x:A) -> A = \ A -> \ x -> A ;