reconsider a = a, b = b as Element of Funcs (Y,BOOLEAN) ;
a 'eqv' b is Element of Funcs (Y,BOOLEAN) ;
hence a 'eqv' b is Element of Funcs (Y,BOOLEAN) ; :: thesis: verum