Hola.
El tipo que ponés en apply2 es correcto pero no se corresponde con el término. En particular "(X:A)" debe ser "(A:Set)". El primer argumento de apply2 debe ser un Set no un elemento de tipo Set. Lo mismo para el otro Set (B).
Definition apply2: forall A B : Set, (A->B)->A->B := fun (A:Set) (B:Set) f n => f n.
Saludos, Carlos